proposition: Lemma all_prodn_gt0 : forall (I : finType) r (P : pred I) (F : I -> nat), (\prod_(i <- r | P i) F i > 0)%N -> forall i, i \in r -> P i -> (F i > 0)%N.
proof: Proof. move=> I r P F; elim: r => [_|a r hr] //. rewrite big_cons; case hPa: (P a). rewrite muln_gt0; case/andP=> Fa0; move/hr=> hF x. by rewrite in_cons; case/orP; [move/eqP-> | move/hF]. move/hr=> hF x; rewrite in_cons; case/orP; last by move/hF. by move/eqP->; rewrite hPa. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice path fintype) mathcomp(div bigop order ssralg poly polydiv ssrnum perm zmodp ssrint) mathcomp(polyorder polyrcf interval matrix mxtens)