monotonous and derivative

[affeldt-aist]

Motivation for this change

This PR contains a proof that "decreasing implies non-positive derivative".
@t6s If I remember correctly, you proved similar lemmas somewhere.
Are they in some pending PRs or do you have them elsewhere?
(By the way, the lemmas in this PR are used to prove integration-by-substitution like lemmas.)

@IshiguroYoshihiro you may want to amend this PR.

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

[t6s]

Yes, I have a local branch for a similar PR, though not ready yet.

I'm happy to have this PR going first, so that I can generalize the lemmas as needed.

[affeldt-aist]

Ah, I remember now. We were actually discussing generalizations of the lemmas that establish monotonicity from the sign of the derivative, as the two lemmas in this commit 2b63e89
(the lemmas in the previous commit are doing the contrary).
I think that you had other variants of the lemmas in the second commit.

Ideally, we want to factorize all of the them as a few generic lemmas exploiting the Interval type.