proposition: Lemma prodf_neq0 (I : finType) (P : pred I) (F : I -> R) : reflect (forall i, P i -> (F i != 0)) (\prod_(i | P i) F i != 0).
proof: Proof. by rewrite (sameP (prodf_eq0 _ _) exists_inP); apply: exists_inPn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)