proposition: Lemma leq_prodn I r (P : pred I) F1 F2 : (forall i, P i -> F1 i <= F2 i) -> \prod_(i <- r | P i) F1 i <= \prod_(i <- r | P i) F2 i.
proof: Proof. move=> leF; elim: r => [| x r ihr] /=; first by rewrite !big_nil. rewrite !big_cons; case: ifP => hPx //; apply: leq_mul => //; exact: leF. Qed.
imports: mathcomp(all_ssreflect all_algebra)