proposition: Lemma leif_pprod (I : finType) (P C : pred I) (E1 E2 : I -> R) : (forall i, P i -> 0 <= E1 i) -> (forall i, P i -> E1 i <= E2 i ?= iff C i) -> let pi E := \prod_(i | P i) E i in pi E1 <= pi E2 ?= iff (pi E2 == 0) || [forall (i | P i), C i].
proof: Proof. move=> E1_ge0 leE12 /=; rewrite -big_andE; elim/(big_load (fun x => 0 <= x)): _. elim/big_rec3: _ => [|i Ci m2 m1 Pi [m1ge0 le_m12]]. by split=> //; apply/leifP; rewrite orbT. have Ei_ge0 := E1_ge0 i Pi; split; first by rewrite mulr_ge0. congr (leif _ _ _): (leif_pM Ei_ge0 m1ge0 (leE12 i Pi) le_m12). by rewrite mulf_eq0 -!orbA; congr (_ || _); rewrite !orb_andr orbA orbb. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)