proposition: Lemma prodf_eq0 (I : finType) (P : pred I) (F : I -> R) : reflect (exists2 i, P i & (F i == 0)) (\prod_(i | P i) F i == 0).
proof: Proof. apply: (iffP idP) => [|[i Pi /eqP Fi0]]; last first. by rewrite (bigD1 i) //= Fi0 mul0r. elim: (index_enum _) => [|i r IHr]; first by rewrite big_nil oner_eq0. rewrite big_cons /=; have [Pi | _] := ifP; last exact: IHr. by rewrite mulf_eq0; case/orP=> // Fi0; exists i. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)