proposition: Lemma Euclid_dvd_prod (I : Type) (r : seq I) (P : pred I) (f : I -> nat) p : prime p -> p %| \prod_(i <- r | P i) f i = \big[orb/false]_(i <- r | P i) (p %| f i).
proof: Proof. move=> pP; apply: big_morph=> [x y|]; [exact: Euclid_dvdM | exact: Euclid_dvd1]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)