proposition: Lemma leif_sum (I : finType) (P C : pred I) (E1 E2 : I -> R) : (forall i, P i -> E1 i <= E2 i ?= iff C i) -> \sum_(i | P i) E1 i <= \sum_(i | P i) E2 i ?= iff [forall (i | P i), C i].
proof: Proof. move=> leE12; rewrite -big_andE. elim/big_rec3: _ => [|i Ci m2 m1 /leE12]; first by rewrite /leif lexx eqxx. exact: leifD. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)