diff options
Diffstat (limited to 'theories7/ZArith/Znumtheory.v')
| -rw-r--r-- | theories7/ZArith/Znumtheory.v | 629 |
1 files changed, 0 insertions, 629 deletions
diff --git a/theories7/ZArith/Znumtheory.v b/theories7/ZArith/Znumtheory.v deleted file mode 100644 index b8e5f300..00000000 --- a/theories7/ZArith/Znumtheory.v +++ /dev/null @@ -1,629 +0,0 @@ -(************************************************************************) -(* 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. - - |