Euclid theorem for product (#375)

1 files changed, 9 insertions, 2 deletions

diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index 7d07293..9eafea9 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -411,14 +411,21 @@ move=> pr_p pr_q; apply: negb_inj.
 by rewrite eqn_dvd negb_and -!prime_coprime // coprime_sym orbb.
 Qed.
 
+Lemma Euclid_dvd1 p : prime p -> (p %| 1) = false.
+Proof. by rewrite dvdn1; case: eqP => // ->. Qed.
+
 Lemma Euclid_dvdM m n p : prime p -> (p %| m * n) = (p %| m) || (p %| n).
 Proof.
 move=> pr_p; case dv_pm: (p %| m); first exact: dvdn_mulr.
 by rewrite Gauss_dvdr // prime_coprime // dv_pm.
 Qed.
 
-Lemma Euclid_dvd1 p : prime p -> (p %| 1) = false.
-Proof. by rewrite dvdn1; case: eqP => // ->. Qed.
+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.
+move=> pP; apply: big_morph=> [x y|]; [exact: Euclid_dvdM | exact: Euclid_dvd1].
+Qed.
 
 Lemma Euclid_dvdX m n p : prime p -> (p %| m ^ n) = (p %| m) && (n > 0).
 Proof.