FTC1 corollary

[affeldt-aist]

Motivation for this change

See issue #965

Provides also the Borel-Cantelli lemma (and the limit superior of the sequence of sets) and continuity of the indefinite integral at the borders (which is maybe the part that is not the cleanest).

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[zstone1]

A couple small comments. Going via "charge_variation is uniformly continuous" is clever indeed. That's a nice trick to stay general for as long as possible.

[affeldt-aist]

@t6s we renamed indefinite_integral to parameterized_integral following the last mathcomp-analysis-dev meeting

[affeldt-aist]

Got an offline approval by Zachary for this PR, will merge soon.