l'hopital's rule

[affeldt-aist]

Motivation for this change

This PR provides a proof of L'Hopital's rule which is more general
than PR #1371 (I did not add a commit to this PR whose log is too complicated
for a proper rebase).

@ndslusarz I kept the previous versions of the lemmas in sections
lhopital0 and lhopital1, you can use them in your development but
it would be much better if you can use instead the lemmas lhopital_at_right and
lhopital_at_left instead.
Can you check that so that we remove them and your development
still stays compatible with the next version of MathComp-Analysis?

(thanks @zstone1)

closes PR #1371

better to merge PR #1477 before this one (fyi @t6s)

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]

What about we merge this one? It addresses @zstone1 's comments and its availability in MathComp-Analysis 1.9.0 could make like easier for @ndslusarz .
@hoheinzollern

[zstone1]

Looks great. Structurally, the left and right versions have "sharp" boundary conditions. The proof of the left one is a short application of the right. And the proof of the two-sided one is a short application as well. Basically as good as we could hope for.