Derivative limit theorem

[nmolinamounier]

Motivation for this change

Split from #2023. Depends on #2026 and #2030. Proves the same result in a nicer way.

Adds the "derivative limit theorem": for $$a \in \mathbb{R}$$ and $$f : \mathbb{R} \to \mathbb{R}$$, if:

1. $$f$$ is continuous at $$a$$
2. $$f$$ is derivable near $$a$$ (but not necessarily at $$a$$)
3. The limit of $$f'(x)$$ as $$x \to a, x \neq a$$ exists and equals $$\ell \in \mathbb{R}$$
   Then $$f$$ is derivable at $$a$$ and $$f'(a) = \ell$$. Also adds sided variants of the result.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

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

[affeldt-aist]

Postponed to next release because of the dependency on PR #2030