natural logarithme for extended real numbers

[affeldt-aist]

Motivation for this change

closes draft PR #1613

@jmmarulang : I have duplicated your PR to avoid pushing on your master

Checklist

• [x] 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]

Note that the last commit changes the definition of lne so that lne -oo = -oo and then we can write

Lemma lne_div : {in `]0, +oo] &, {morph lne : x y / x / y >-> x - y}}.

instead of

Lemma lne_div x y :
  0 < x -> 0 < y -> lne (x * (fine y)^-1%:E) = lne x - lne y.

(fyi: @CohenCyril)

@jmmarulang It looks a bit better but is it as useful to you?

[affeldt-aist]

This PR has been discussed, already been approved, CI errors seem unrelated, and comments have been addressed.

@jmmarulang and @hoheinzollern , you may want to take a last look before squash-merge.

@proux01 there is a minor fix in constructive_ereal.v, as a big contributor to this file you maybe want to double-check

[proux01]

CI errors seem unrelated

I agree but let me rebase it to be extra safe.

[proux01]

@affeldt-aist CI green, I let you squash / merge at your convenience

[affeldt-aist]

@affeldt-aist CI green, I let you squash / merge at your convenience

Thanks! (I wait a bit for input by the other participants to the conversation.)

[proux01]

So, apparently I was right to want to get green CI but this wasn't enough. This PR ended up in a strange situation where this doesn't compile on MC master with Rocq <= 9.1, a combination we didn't test since we only test MC master on Rocq master. C.f. https://github.com/math-comp/analysis/pull/1703