diff options
Diffstat (limited to 'theories7/ZArith/Znumtheory.v')
| -rw-r--r-- | theories7/ZArith/Znumtheory.v | 629 |
1 files changed, 629 insertions, 0 deletions
diff --git a/theories7/ZArith/Znumtheory.v b/theories7/ZArith/Znumtheory.v new file mode 100644 index 00000000..b8e5f300 --- /dev/null +++ b/theories7/ZArith/Znumtheory.v @@ -0,0 +1,629 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Znumtheory.v,v 1.3.2.1 2004/07/16 19:31:43 herbelin Exp $ i*) + +Require ZArith_base. +Require ZArithRing. +Require Zcomplements. +Require Zdiv. +V7only [Import Z_scope.]. +Open Local Scope Z_scope. + +(** This file contains some notions of number theory upon Z numbers: + - a divisibility predicate [Zdivide] + - a gcd predicate [gcd] + - Euclid algorithm [euclid] + - an efficient [Zgcd] function + - a relatively prime predicate [rel_prime] + - a prime predicate [prime] +*) + +(** * Divisibility *) + +Inductive Zdivide [a,b:Z] : Prop := + Zdivide_intro : (q:Z) `b = q * a` -> (Zdivide a b). + +(** Syntax for divisibility *) + +Notation "( a | b )" := (Zdivide a b) + (at level 0, a,b at level 10) : Z_scope + V8only "( a | b )" (at level 0). + +(** Results concerning divisibility*) + +Lemma Zdivide_refl : (a:Z) (a|a). +Proof. +Intros; Apply Zdivide_intro with `1`; Ring. +Save. + +Lemma Zone_divide : (a:Z) (1|a). +Proof. +Intros; Apply Zdivide_intro with `a`; Ring. +Save. + +Lemma Zdivide_0 : (a:Z) (a|0). +Proof. +Intros; Apply Zdivide_intro with `0`; Ring. +Save. + +Hints Resolve Zdivide_refl Zone_divide Zdivide_0 : zarith. + +Lemma Zdivide_mult_left : (a,b,c:Z) (a|b) -> (`c*a`|`c*b`). +Proof. +Induction 1; Intros; Apply Zdivide_intro with q. +Rewrite H0; Ring. +Save. + +Lemma Zdivide_mult_right : (a,b,c:Z) (a|b) -> (`a*c`|`b*c`). +Proof. +Intros a b c; Rewrite (Zmult_sym a c); Rewrite (Zmult_sym b c). +Apply Zdivide_mult_left; Trivial. +Save. + +Hints Resolve Zdivide_mult_left Zdivide_mult_right : zarith. + +Lemma Zdivide_plus : (a,b,c:Z) (a|b) -> (a|c) -> (a|`b+c`). +Proof. +Induction 1; Intros q Hq; Induction 1; Intros q' Hq'. +Apply Zdivide_intro with `q+q'`. +Rewrite Hq; Rewrite Hq'; Ring. +Save. + +Lemma Zdivide_opp : (a,b:Z) (a|b) -> (a|`-b`). +Proof. +Induction 1; Intros; Apply Zdivide_intro with `-q`. +Rewrite H0; Ring. +Save. + +Lemma Zdivide_opp_rev : (a,b:Z) (a|`-b`) -> (a| b). +Proof. +Intros; Replace b with `-(-b)`. Apply Zdivide_opp; Trivial. Ring. +Save. + +Lemma Zdivide_opp_left : (a,b:Z) (a|b) -> (`-a`|b). +Proof. +Induction 1; Intros; Apply Zdivide_intro with `-q`. +Rewrite H0; Ring. +Save. + +Lemma Zdivide_opp_left_rev : (a,b:Z) (`-a`|b) -> (a|b). +Proof. +Intros; Replace a with `-(-a)`. Apply Zdivide_opp_left; Trivial. Ring. +Save. + +Lemma Zdivide_minus : (a,b,c:Z) (a|b) -> (a|c) -> (a|`b-c`). +Proof. +Induction 1; Intros q Hq; Induction 1; Intros q' Hq'. +Apply Zdivide_intro with `q-q'`. +Rewrite Hq; Rewrite Hq'; Ring. +Save. + +Lemma Zdivide_left : (a,b,c:Z) (a|b) -> (a|`b*c`). +Proof. +Induction 1; Intros q Hq; Apply Zdivide_intro with `q*c`. +Rewrite Hq; Ring. +Save. + +Lemma Zdivide_right : (a,b,c:Z) (a|c) -> (a|`b*c`). +Proof. +Induction 1; Intros q Hq; Apply Zdivide_intro with `q*b`. +Rewrite Hq; Ring. +Save. + +Lemma Zdivide_a_ab : (a,b:Z) (a|`a*b`). +Proof. +Intros; Apply Zdivide_intro with b; Ring. +Save. + +Lemma Zdivide_a_ba : (a,b:Z) (a|`b*a`). +Proof. +Intros; Apply Zdivide_intro with b; Ring. +Save. + +Hints Resolve Zdivide_plus Zdivide_opp Zdivide_opp_rev + Zdivide_opp_left Zdivide_opp_left_rev + Zdivide_minus Zdivide_left Zdivide_right + Zdivide_a_ab Zdivide_a_ba : zarith. + +(** Auxiliary result. *) + +Lemma Zmult_one : + (x,y:Z) `x>=0` -> `x*y=1` -> `x=1`. +Proof. +Intros x y H H0; NewDestruct (Zmult_1_inversion_l ? ? H0) as [Hpos|Hneg]. + Assumption. + Rewrite Hneg in H; Simpl in H. + Contradiction (Zle_not_lt `0` `-1`). + Apply Zge_le; Assumption. + Apply NEG_lt_ZERO. +Save. + +(** Only [1] and [-1] divide [1]. *) + +Lemma Zdivide_1 : (x:Z) (x|1) -> `x=1` \/ `x=-1`. +Proof. +Induction 1; Intros. +Elim (Z_lt_ge_dec `0` x); [Left|Right]. +Apply Zmult_one with q; Auto with zarith; Rewrite H0; Ring. +Assert `(-x) = 1`; Auto with zarith. +Apply Zmult_one with (-q); Auto with zarith; Rewrite H0; Ring. +Save. + +(** If [a] divides [b] and [b] divides [a] then [a] is [b] or [-b]. *) + +Lemma Zdivide_antisym : (a,b:Z) (a|b) -> (b|a) -> `a=b` \/ `a=-b`. +Proof. +Induction 1; Intros. +Inversion H1. +Rewrite H0 in H2; Clear H H1. +Case (Z_zerop a); Intro. +Left; Rewrite H0; Rewrite e; Ring. +Assert Hqq0: `q0*q = 1`. +Apply Zmult_reg_left with a. +Assumption. +Ring. +Pattern 2 a; Rewrite H2; Ring. +Assert (q|1). +Rewrite <- Hqq0; Auto with zarith. +Elim (Zdivide_1 q H); Intros. +Rewrite H1 in H0; Left; Omega. +Rewrite H1 in H0; Right; Omega. +Save. + +(** If [a] divides [b] and [b<>0] then [|a| <= |b|]. *) + +Lemma Zdivide_bounds : (a,b:Z) (a|b) -> `b<>0` -> `|a| <= |b|`. +Proof. +Induction 1; Intros. +Assert `|b|=|q|*|a|`. + Subst; Apply Zabs_Zmult. +Rewrite H2. +Assert H3 := (Zabs_pos q). +Assert H4 := (Zabs_pos a). +Assert `|q|*|a|>=1*|a|`; Auto with zarith. +Apply Zge_Zmult_pos_compat; Auto with zarith. +Elim (Z_lt_ge_dec `|q|` `1`); [ Intros | Auto with zarith ]. +Assert `|q|=0`. + Omega. +Assert `q=0`. + Rewrite <- (Zabs_Zsgn q). +Rewrite H5; Auto with zarith. +Subst q; Omega. +Save. + +(** * Greatest common divisor (gcd). *) + +(** There is no unicity of the gcd; hence we define the predicate [gcd a b d] + expressing that [d] is a gcd of [a] and [b]. + (We show later that the [gcd] is actually unique if we discard its sign.) *) + +Inductive gcd [a,b,d:Z] : Prop := + gcd_intro : + (d|a) -> (d|b) -> ((x:Z) (x|a) -> (x|b) -> (x|d)) -> (gcd a b d). + +(** Trivial properties of [gcd] *) + +Lemma gcd_sym : (a,b,d:Z)(gcd a b d) -> (gcd b a d). +Proof. +Induction 1; Constructor; Intuition. +Save. + +Lemma gcd_0 : (a:Z)(gcd a `0` a). +Proof. +Constructor; Auto with zarith. +Save. + +Lemma gcd_minus :(a,b,d:Z)(gcd a `-b` d) -> (gcd b a d). +Proof. +Induction 1; Constructor; Intuition. +Save. + +Lemma gcd_opp :(a,b,d:Z)(gcd a b d) -> (gcd b a `-d`). +Proof. +Induction 1; Constructor; Intuition. +Save. + +Hints Resolve gcd_sym gcd_0 gcd_minus gcd_opp : zarith. + +(** * Extended Euclid algorithm. *) + +(** Euclid's algorithm to compute the [gcd] mainly relies on + the following property. *) + +Lemma gcd_for_euclid : + (a,b,d,q:Z) (gcd b `a-q*b` d) -> (gcd a b d). +Proof. +Induction 1; Constructor; Intuition. +Replace a with `a-q*b+q*b`. Auto with zarith. Ring. +Save. + +Lemma gcd_for_euclid2 : + (b,d,q,r:Z) (gcd r b d) -> (gcd b `b*q+r` d). +Proof. +Induction 1; Constructor; Intuition. +Apply H2; Auto. +Replace r with `b*q+r-b*q`. Auto with zarith. Ring. +Save. + +(** We implement the extended version of Euclid's algorithm, + i.e. the one computing Bezout's coefficients as it computes + the [gcd]. We follow the algorithm given in Knuth's + "Art of Computer Programming", vol 2, page 325. *) + +Section extended_euclid_algorithm. + +Variable a,b : Z. + +(** The specification of Euclid's algorithm is the existence of + [u], [v] and [d] such that [ua+vb=d] and [(gcd a b d)]. *) + +Inductive Euclid : Set := + Euclid_intro : + (u,v,d:Z) `u*a+v*b=d` -> (gcd a b d) -> Euclid. + +(** The recursive part of Euclid's algorithm uses well-founded + recursion of non-negative integers. It maintains 6 integers + [u1,u2,u3,v1,v2,v3] such that the following invariant holds: + [u1*a+u2*b=u3] and [v1*a+v2*b=v3] and [gcd(u2,v3)=gcd(a,b)]. + *) + +Lemma euclid_rec : + (v3:Z) `0 <= v3` -> (u1,u2,u3,v1,v2:Z) `u1*a+u2*b=u3` -> `v1*a+v2*b=v3` -> + ((d:Z)(gcd u3 v3 d) -> (gcd a b d)) -> Euclid. +Proof. +Intros v3 Hv3; Generalize Hv3; Pattern v3. +Apply Z_lt_rec. +Clear v3 Hv3; Intros. +Elim (Z_zerop x); Intro. +Apply Euclid_intro with u:=u1 v:=u2 d:=u3. +Assumption. +Apply H2. +Rewrite a0; Auto with zarith. +LetTac q := (Zdiv u3 x). +Assert Hq: `0 <= u3-q*x < x`. +Replace `u3-q*x` with `u3%x`. +Apply Z_mod_lt; Omega. +Assert xpos : `x > 0`. Omega. +Generalize (Z_div_mod_eq u3 x xpos). +Unfold q. +Intro eq; Pattern 2 u3; Rewrite eq; Ring. +Apply (H `u3-q*x` Hq (proj1 ? ? Hq) v1 v2 x `u1-q*v1` `u2-q*v2`). +Tauto. +Replace `(u1-q*v1)*a+(u2-q*v2)*b` with `(u1*a+u2*b)-q*(v1*a+v2*b)`. +Rewrite H0; Rewrite H1; Trivial. +Ring. +Intros; Apply H2. +Apply gcd_for_euclid with q; Assumption. +Assumption. +Save. + +(** We get Euclid's algorithm by applying [euclid_rec] on + [1,0,a,0,1,b] when [b>=0] and [1,0,a,0,-1,-b] when [b<0]. *) + +Lemma euclid : Euclid. +Proof. +Case (Z_le_gt_dec `0` b); Intro. +Intros; Apply euclid_rec with u1:=`1` u2:=`0` u3:=a + v1:=`0` v2:=`1` v3:=b; +Auto with zarith; Ring. +Intros; Apply euclid_rec with u1:=`1` u2:=`0` u3:=a + v1:=`0` v2:=`-1` v3:=`-b`; +Auto with zarith; Try Ring. +Save. + +End extended_euclid_algorithm. + +Theorem gcd_uniqueness_apart_sign : + (a,b,d,d':Z) (gcd a b d) -> (gcd a b d') -> `d = d'` \/ `d = -d'`. +Proof. +Induction 1. +Intros H1 H2 H3; Induction 1; Intros. +Generalize (H3 d' H4 H5); Intro Hd'd. +Generalize (H6 d H1 H2); Intro Hdd'. +Exact (Zdivide_antisym d d' Hdd' Hd'd). +Save. + +(** * Bezout's coefficients *) + +Inductive Bezout [a,b,d:Z] : Prop := + Bezout_intro : (u,v:Z) `u*a + v*b = d` -> (Bezout a b d). + +(** Existence of Bezout's coefficients for the [gcd] of [a] and [b] *) + +Lemma gcd_bezout : (a,b,d:Z) (gcd a b d) -> (Bezout a b d). +Proof. +Intros a b d Hgcd. +Elim (euclid a b); Intros u v d0 e g. +Generalize (gcd_uniqueness_apart_sign a b d d0 Hgcd g). +Intro H; Elim H; Clear H; Intros. +Apply Bezout_intro with u v. +Rewrite H; Assumption. +Apply Bezout_intro with `-u` `-v`. +Rewrite H; Rewrite <- e; Ring. +Save. + +(** gcd of [ca] and [cb] is [c gcd(a,b)]. *) + +Lemma gcd_mult : (a,b,c,d:Z) (gcd a b d) -> (gcd `c*a` `c*b` `c*d`). +Proof. +Intros a b c d; Induction 1; Constructor; Intuition. +Elim (gcd_bezout a b d H); Intros. +Elim H3; Intros. +Elim H4; Intros. +Apply Zdivide_intro with `u*q+v*q0`. +Rewrite <- H5. +Replace `c*(u*a+v*b)` with `u*(c*a)+v*(c*b)`. +Rewrite H6; Rewrite H7; Ring. +Ring. +Save. + +(** We could obtain a [Zgcd] function via [euclid]. But we propose + here a more direct version of a [Zgcd], with better extraction + (no bezout coeffs). *) + +Definition Zgcd_pos : (a:Z)`0<=a` -> (b:Z) + { g:Z | `0<=a` -> (gcd a b g) /\ `g>=0` }. +Proof. +Intros a Ha. +Apply (Z_lt_rec [a:Z](b:Z) { g:Z | `0<=a` -> (gcd a b g) /\`g>=0` }); Try Assumption. +Intro x; Case x. +Intros _ b; Exists (Zabs b). + Elim (Z_le_lt_eq_dec ? ? (Zabs_pos b)). + Intros H0; Split. + Apply Zabs_ind. + Intros; Apply gcd_sym; Apply gcd_0; Auto. + Intros; Apply gcd_opp; Apply gcd_0; Auto. + Auto with zarith. + + Intros H0; Rewrite <- H0. + Rewrite <- (Zabs_Zsgn b); Rewrite <- H0; Simpl. + Split; [Apply gcd_0|Idtac];Auto with zarith. + +Intros p Hrec b. +Generalize (Z_div_mod b (POS p)). +Case (Zdiv_eucl b (POS p)); Intros q r Hqr. +Elim Hqr; Clear Hqr; Intros; Auto with zarith. +Elim (Hrec r H0 (POS p)); Intros g Hgkl. +Inversion_clear H0. +Elim (Hgkl H1); Clear Hgkl; Intros H3 H4. +Exists g; Intros. +Split; Auto. +Rewrite H. +Apply gcd_for_euclid2; Auto. + +Intros p Hrec b. +Exists `0`; Intros. +Elim H; Auto. +Defined. + +Definition Zgcd_spec : (a,b:Z){ g : Z | (gcd a b g) /\ `g>=0` }. +Proof. +Intros a; Case (Z_gt_le_dec `0` a). +Intros; Assert `0 <= -a`. +Omega. +Elim (Zgcd_pos `-a` H b); Intros g Hgkl. +Exists g. +Intuition. +Intros Ha b; Elim (Zgcd_pos a Ha b); Intros g; Exists g; Intuition. +Defined. + +Definition Zgcd := [a,b:Z](let (g,_) = (Zgcd_spec a b) in g). + +Lemma Zgcd_is_pos : (a,b:Z)`(Zgcd a b) >=0`. +Intros a b; Unfold Zgcd; Case (Zgcd_spec a b); Tauto. +Qed. + +Lemma Zgcd_is_gcd : (a,b:Z)(gcd a b (Zgcd a b)). +Intros a b; Unfold Zgcd; Case (Zgcd_spec a b); Tauto. +Qed. + +(** * Relative primality *) + +Definition rel_prime [a,b:Z] : Prop := (gcd a b `1`). + +(** Bezout's theorem: [a] and [b] are relatively prime if and + only if there exist [u] and [v] such that [ua+vb = 1]. *) + +Lemma rel_prime_bezout : + (a,b:Z) (rel_prime a b) -> (Bezout a b `1`). +Proof. +Intros a b; Exact (gcd_bezout a b `1`). +Save. + +Lemma bezout_rel_prime : + (a,b:Z) (Bezout a b `1`) -> (rel_prime a b). +Proof. +Induction 1; Constructor; Auto with zarith. +Intros. Rewrite <- H0; Auto with zarith. +Save. + +(** Gauss's theorem: if [a] divides [bc] and if [a] and [b] are + relatively prime, then [a] divides [c]. *) + +Theorem Gauss : (a,b,c:Z) (a |`b*c`) -> (rel_prime a b) -> (a | c). +Proof. +Intros. Elim (rel_prime_bezout a b H0); Intros. +Replace c with `c*1`; [ Idtac | Ring ]. +Rewrite <- H1. +Replace `c*(u*a+v*b)` with `(c*u)*a + v*(b*c)`; [ EAuto with zarith | Ring ]. +Save. + +(** If [a] is relatively prime to [b] and [c], then it is to [bc] *) + +Lemma rel_prime_mult : + (a,b,c:Z) (rel_prime a b) -> (rel_prime a c) -> (rel_prime a `b*c`). +Proof. +Intros a b c Hb Hc. +Elim (rel_prime_bezout a b Hb); Intros. +Elim (rel_prime_bezout a c Hc); Intros. +Apply bezout_rel_prime. +Apply Bezout_intro with u:=`u*u0*a+v0*c*u+u0*v*b` v:=`v*v0`. +Rewrite <- H. +Replace `u*a+v*b` with `(u*a+v*b) * 1`; [ Idtac | Ring ]. +Rewrite <- H0. +Ring. +Save. + +Lemma rel_prime_cross_prod : + (a,b,c,d:Z) (rel_prime a b) -> (rel_prime c d) -> `b>0` -> `d>0` -> + `a*d = b*c` -> (a=c /\ b=d). +Proof. +Intros a b c d; Intros. +Elim (Zdivide_antisym b d). +Split; Auto with zarith. +Rewrite H4 in H3. +Rewrite Zmult_sym in H3. +Apply Zmult_reg_left with d; Auto with zarith. +Intros; Omega. +Apply Gauss with a. +Rewrite H3. +Auto with zarith. +Red; Auto with zarith. +Apply Gauss with c. +Rewrite Zmult_sym. +Rewrite <- H3. +Auto with zarith. +Red; Auto with zarith. +Save. + +(** After factorization by a gcd, the original numbers are relatively prime. *) + +Lemma gcd_rel_prime : + (a,b,g:Z)`b>0` -> `g>=0`-> (gcd a b g) -> (rel_prime `a/g` `b/g`). +Intros a b g; Intros. +Assert `g <> 0`. + Intro. + Elim H1; Intros. + Elim H4; Intros. + Rewrite H2 in H6; Subst b; Omega. +Unfold rel_prime. +Elim (Zgcd_spec `a/g` `b/g`); Intros g' (H3,H4). +Assert H5 := (gcd_mult ? ? g ? H3). +Rewrite <- Z_div_exact_2 in H5; Auto with zarith. +Rewrite <- Z_div_exact_2 in H5; Auto with zarith. +Elim (gcd_uniqueness_apart_sign ? ? ? ? H1 H5). +Intros; Rewrite (!Zmult_reg_left `1` g' g); Auto with zarith. +Intros; Rewrite (!Zmult_reg_left `1` `-g'` g); Auto with zarith. +Pattern 1 g; Rewrite H6; Ring. + +Elim H1; Intros. +Elim H7; Intros. +Rewrite H9. +Replace `q*g` with `0+q*g`. +Rewrite Z_mod_plus. +Compute; Auto. +Omega. +Ring. + +Elim H1; Intros. +Elim H6; Intros. +Rewrite H9. +Replace `q*g` with `0+q*g`. +Rewrite Z_mod_plus. +Compute; Auto. +Omega. +Ring. +Save. + +(** * Primality *) + +Inductive prime [p:Z] : Prop := + prime_intro : + `1 < p` -> ((n:Z) `1 <= n < p` -> (rel_prime n p)) -> (prime p). + +(** The sole divisors of a prime number [p] are [-1], [1], [p] and [-p]. *) + +Lemma prime_divisors : + (p:Z) (prime p) -> + (a:Z) (a|p) -> `a = -1` \/ `a = 1` \/ a = p \/ `a = -p`. +Proof. +Induction 1; Intros. +Assert `a = (-p)`\/`-p<a< -1`\/`a = -1`\/`a=0`\/`a = 1`\/`1<a<p`\/`a = p`. +Assert `|a| <= |p|`. Apply Zdivide_bounds; [ Assumption | Omega ]. +Generalize H3. +Pattern `|a|`; Apply Zabs_ind; Pattern `|p|`; Apply Zabs_ind; Intros; Omega. +Intuition Idtac. +(* -p < a < -1 *) +Absurd (rel_prime `-a` p); Intuition. +Inversion H3. +Assert (`-a` | `-a`); Auto with zarith. +Assert (`-a` | p); Auto with zarith. +Generalize (H8 `-a` H9 H10); Intuition Idtac. +Generalize (Zdivide_1 `-a` H11); Intuition. +(* a = 0 *) +Inversion H2. Subst a; Omega. +(* 1 < a < p *) +Absurd (rel_prime a p); Intuition. +Inversion H3. +Assert (a | a); Auto with zarith. +Assert (a | p); Auto with zarith. +Generalize (H8 a H9 H10); Intuition Idtac. +Generalize (Zdivide_1 a H11); Intuition. +Save. + +(** A prime number is relatively prime with any number it does not divide *) + +Lemma prime_rel_prime : + (p:Z) (prime p) -> (a:Z) ~ (p|a) -> (rel_prime p a). +Proof. +Induction 1; Intros. +Constructor; Intuition. +Elim (prime_divisors p H x H3); Intuition; Subst; Auto with zarith. +Absurd (p | a); Auto with zarith. +Absurd (p | a); Intuition. +Save. + +Hints Resolve prime_rel_prime : zarith. + +(** [Zdivide] can be expressed using [Zmod]. *) + +Lemma Zmod_Zdivide : (a,b:Z) `b>0` -> `a%b = 0` -> (b|a). +Intros a b H H0. +Apply Zdivide_intro with `(a/b)`. +Pattern 1 a; Rewrite (Z_div_mod_eq a b H). +Rewrite H0; Ring. +Save. + +Lemma Zdivide_Zmod : (a,b:Z) `b>0` -> (b|a) -> `a%b = 0`. +Intros a b; Destruct 2; Intros; Subst. +Change `q*b` with `0+q*b`. +Rewrite Z_mod_plus; Auto. +Save. + +(** [Zdivide] is hence decidable *) + +Lemma Zdivide_dec : (a,b:Z) { (a|b) } + { ~ (a|b) }. +Proof. +Intros a b; Elim (Ztrichotomy_inf a `0`). +(* a<0 *) +Intros H; Elim H; Intros. +Case (Z_eq_dec `b%(-a)` `0`). +Left; Apply Zdivide_opp_left_rev; Apply Zmod_Zdivide; Auto with zarith. +Intro H1; Right; Intro; Elim H1; Apply Zdivide_Zmod; Auto with zarith. +(* a=0 *) +Case (Z_eq_dec b `0`); Intro. +Left; Subst; Auto with zarith. +Right; Subst; Intro H0; Inversion H0; Omega. +(* a>0 *) +Intro H; Case (Z_eq_dec `b%a` `0`). +Left; Apply Zmod_Zdivide; Auto with zarith. +Intro H1; Right; Intro; Elim H1; Apply Zdivide_Zmod; Auto with zarith. +Save. + +(** If a prime [p] divides [ab] then it divides either [a] or [b] *) + +Lemma prime_mult : + (p:Z) (prime p) -> (a,b:Z) (p | `a*b`) -> (p | a) \/ (p | b). +Proof. +Intro p; Induction 1; Intros. +Case (Zdivide_dec p a); Intuition. +Right; Apply Gauss with a; Auto with zarith. +Save. + + |