tentative generalization of FTC2

[affeldt-aist]

Motivation for this change

• for continuous function on unbounded intervals
• by-product of the Gauss integral (in the sense that it used to prove it in a forthcoming PR (that shall provide yet another proof of the Gauss integral))

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

[affeldt-aist]

@IshiguroYoshihiro Can you check if there are generalizations you wanted to do?

[t6s]

Looks good. Latexified doc for the added lemmas will help the user, but it can be done in a separate PR.

[affeldt-aist]

Looks good. Latexified doc for the added lemmas will help the user, but it can be done in a separate PR.

Something like that? (fyi @proux01 )

[t6s]

Looks good. Latexified doc for the added lemmas will help the user, but it can be done in a separate PR.

Something like that? (fyi @proux01 )

This looks very nice! There are subtle lists of hypotheses for each of these lemmas, and clarifying them by latex will be also useful.

[affeldt-aist]

There are subtle lists of hypotheses for each of these lemmas, and clarifying them by latex will be also useful.

I was reluctant to do that because I thought that from a user point of view it is enough to know about the lemma is about and to check the exact hypotheses by going to where it is defined in the file. What about just emphasizing that the reader should go to the formal statement for the exact set of hypotheses?

[t6s]

Let us keep the header simple and contain only the objective of lemmas. I think I am agreeing with you on this point.
I don't think that emphasis about hypotheses is not particularly necessary because Coq will appropriately show the formal
hypotheses to the user when needed.

A desirable interface for the hypotheses would be to latex-render them when the user issues the About command,
with the markdown source for that rendering provided by the developer at each statement of lemmas.
(I remember @ybertot once suggested adding to Coq such a facility for adding extra comments to lemmas.)

Anyway, I think this PR is ready to be merged.

[affeldt-aist]

A desirable interface for the hypotheses would be to latex-render them when the user issues the About command

which is something for which @CohenCyril might have a solution