proposition: Lemma ler_prod I r (P : pred I) (E1 E2 : I -> R) : (forall i, P i -> 0 <= E1 i <= E2 i) -> \prod_(i <- r | P i) E1 i <= \prod_(i <- r | P i) E2 i.
proof: Proof. move=> leE12; elim/(big_load (fun x => 0 <= x)): _. elim/big_rec2: _ => // i x2 x1 /leE12/andP[le0Ei leEi12] [x1ge0 le_x12]. by rewrite mulr_ge0 // ler_pM. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)