proposition: Lemma ltr_prod I r (P : pred I) (E1 E2 : I -> R) : has P 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. elim: r => //= i r IHr; rewrite !big_cons; case: ifP => {IHr}// Pi _ ltE12. have /andP[le0E1i ltE12i] := ltE12 i Pi; set E2r := \prod_(j <- r | P j) E2 j. apply: le_lt_trans (_ : E1 i * E2r < E2 i * E2r). by rewrite ler_wpM2l ?ler_prod // => j /ltE12/andP[-> /ltW]. by rewrite ltr_pM2r ?prodr_gt0 // => j /ltE12/andP[le0E1j /le_lt_trans->]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)