proposition: Lemma myprodf_eq0 (S : idomainType)(I : eqType) (r : seq I) P (F : I -> S) : reflect (exists2 i, ((i \in r) && (P i)) & (F i == 0)) (\prod_(i <- r| P i) F i == 0).
proof: Proof. apply: (iffP idP) => [|[i Pi /eqP Fi0]]; last first. by case/andP: Pi => ri Pi; rewrite (big_rem _ ri) /= Pi Fi0 mul0r. elim: r => [|i r IHr]; first by rewrite big_nil oner_eq0. rewrite big_cons /=; have [Pi | ?] := ifP. rewrite mulf_eq0; case/orP=> [Fi0|]; first by exists i => //; rewrite mem_head. by case/IHr=> j /andP [rj Pj] Fj; exists j; rewrite // in_cons rj orbT. by case/IHr=> j /andP [rj Pj] Fj; exists j; rewrite // in_cons rj orbT. 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)