Add set of lemmas for esum

[lyonel2017]

Motivation for this change

Set of lemmas for esum extracted from #2049.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

Sorry for the random, minor comments.
Yet, I am already concerned by the fact that we have summable defined both in esum.v and in realsum.v: we might want to distinguish one or the other by adding a small e or a small r in the identifier.

[affeldt-aist]

I made a first pass. I have not yet looked at section esum_summable.
I'll complete this review asap.

Maybe we do not need pos_neq0_esum
(btw, let's keep the substring pos_esum in identifiers
so that we remember easily that we are inside the PosEsum module)
since it is not used and in fact the more general
version neq0_esum (rather: esum_neq0) does not require
non-negativity as an hypothesis
(so far, the rationale was to use the PosEsum module to hold
restricted versions of esum lemmas for non-negative functions).

pos_sum_esum_ge: we can suppress because this is really
just a special case of pos_esum_ge and is used only once.

summable_muleC is maybe not necessary since it is really
just under eq_fun do rewrite muleC

Pending:
pos_esum_ge1/esum_ge1: there might be a better name
(_ge1 looks too much like 1 <= _) but I have not idea yet

esum_unit does not mention unit, maybe esum_if_eq_op_set1
but the script is so short that maybe the lemma is not really useful

TODO: the changelog should mention that le_esum has been generalized

fyi: @strub

[affeldt-aist]

Thank you very much for having taken the time to sort out these lemmas!

I have generalized lemmas (e.g., eq_summable (now eq_esummable),
le_summable (now le_esummable) to use {in D, f = g} instead of f =1 g, etc.).

esummable_esumZ_pos is not a Let: it is used to prove a more general lemma.

I have added esummable_esum_funeneg since we have its counterpart.

esum_posneg has been renamed esumE and used to simplify
proof (by not making appeared the "positive" version).

I also used the new lemmas to simplify a bit realsum.v.

I have not yet checked whether le_esum_fine and le_pos_esum_fine
are really useful but we will use them in a future PR so we can defer this
discussion.

I haven't found a better name for esum_ge1.

Unless somebody jumps in (@strub , @t6s ?), we'll merge soon.