proposition: Lemma ltr_prod_nat (E1 E2 : nat -> R) (n m : nat) : (m < n)%N -> (forall i, (m <= i < n)%N -> 0 <= E1 i < E2 i) -> \prod_(m <= i < n) E1 i < \prod_(m <= i < n) E2 i.
proof: Proof. move=> lt_mn ltE12; rewrite !big_nat ltr_prod {ltE12}//. by apply/hasP; exists m; rewrite ?mem_index_iota leqnn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)