Derivative limit theorem

[amolinamounier]

Motivation for this change

Split from #2023. Depends on #2026 and #2030. Adds the "derivative limit theorem" (informal name, is there a more established one?). It states that, 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$$.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md
• Merge new derive.v lemmas #2026
• Merge normed type neighborhood lemmas #2030

• 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