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]

Suggested change

	Lemma pos_esum_ge1 (I : set T) (f: T -> \bar R) :
	Lemma pos_esum_ge1 (I : set T) (f : T -> \bar R) :

[affeldt-aist]

Suggested change

	\esum_(i in I) a i <> 0 -> exists i, a i <> 0.
	\esum_(i in I) a i <> 0 -> exists i, a i <> 0.

[affeldt-aist]

Can't this be generalized to any A : set U and B : set T?

[affeldt-aist]

This lemma does not look necessary since it is essentially ge0_esum.

[affeldt-aist]

Suggested change

	(* Lemma le_esum S f g : (forall x, S x -> 0 <= f x) -> *)
	(* (forall x, S x -> f x <= g x) -> *)
	(* \esum_(x in S) f x <= \esum_(x in S) g x. *)
	(* Proof. *)
	(* move=> f0 leS; have g0 x : S x -> 0 <= g x. *)
	(* by move=> /[dup] Ax /leS; apply: le_trans; exact: f0 Ax. *)
	(* by rewrite !ge0_esum// PosEsum.le_pos_esum. *)
	(* Qed. *)

[affeldt-aist]

Suggested change

	rewrite esum_if_eq_op.
	by rewrite esum_set1.
	rewrite esum_if_eq_op.
	by rewrite esum_set1.

[affeldt-aist]

Suggested change

	\esum_(i in I) a i <> 0 -> exists i, a i <> 0.
	\esum_(i in I) a i <> 0 -> exists i, a i <> 0.

[affeldt-aist]

Suggested change

	Lemma esum_ge1 {R : realType} {T : choiceType} (I : set T) (f: T -> \bar R) :
	Lemma esum_ge1 {R : realType} {T : choiceType} (I : set T) (f : T -> \bar R) :

[affeldt-aist]

Use exists2 is often a good idea.

[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.