new derive.v lemmas

[amolinamounier]

Motivation for this change

Split from #2023. Depends on #2024, #2025 and #2029. Adds:

• derive1Dn : f^`(i+j) = f^`(j)^`(i)
• derivation of functions of the form fun x => k x *: f x (suffix ZLR)
• derivation of shifted functions (suffix shiftf)
• instance is_derive_exp
• near_equality lemmas for derive1 and derive1n

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md
• Merge Utility lemmas in filter.v #2024
• Merge move is_deriveV and is_derive1_comp to derive.v  #2025
• Merge normed module identity convergence lemmas #2029

• 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