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