missing lemmas about ereal

[affeldt-aist]

Motivation for this change

just noticed a missing lemma in constructive_ereal.v that helps shorten a proof

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

[proux01]

We need the dual addition versions but otherwise looks good to me.

[affeldt-aist]

The dual lemmas have not been updated to the new naming scheme (my fault).
Shall we rename, say, lee_dadd to leedD or lee_dD (maybe more readable for lemmas with longer suffixes)?

[proux01]

I agree the latter is more readable.

[affeldt-aist]

Then I'll do the renaming along this PR.

[proux01]

Thanks a lot!

[affeldt-aist]

Lemmas in the dual version should be aligned.

[proux01]

A few details but otherwise LGTM