Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import ZArith_base.
Require Import ZArithRing.
Require Import Zcomplements.
Require Import Zdiv.
Require Import Wf_nat.

For compatibility reasons, this Open Scope isn't local as it should

Open Scope Z_scope.

This file contains some notions of number theory upon Z numbers:

a divisibility predicate Z.divide
a gcd predicate gcd
Euclid algorithm euclid
a relatively prime predicate rel_prime
a prime predicate prime
properties of the efficient Z.gcd function

The former specialized inductive predicate Z.divide is now a generic existential predicate.

Its former constructor is now a pseudo-constructor.

Definition Zdivide_intro a b q (H:b=q*a) : Z.divide a b := ex_intro _ q H.

Results concerning divisibility

Notation Zone_divide := Z.divide_1_l (only parsing).
Notation Zdivide_0 := Z.divide_0_r (only parsing).
Notation Zmult_divide_compat_l := Z.mul_divide_mono_l (only parsing).
Notation Zmult_divide_compat_r := Z.mul_divide_mono_r (only parsing).
Notation Zdivide_plus_r := Z.divide_add_r (only parsing).
Notation Zdivide_minus_l := Z.divide_sub_r (only parsing).
Notation Zdivide_mult_l := Z.divide_mul_l (only parsing).
Notation Zdivide_mult_r := Z.divide_mul_r (only parsing).
Notation Zdivide_factor_r := Z.divide_factor_l (only parsing).
Notation Zdivide_factor_l := Z.divide_factor_r (only parsing).

Lemma Zdivide_opp_r a b : (a | b) -> (a | - b).a, b:Z
(a | b) -> (a | - b)
Proof.a, b:Z
(a | b) -> (a | - b) apply Z.divide_opp_r. Qed.

Lemma Zdivide_opp_r_rev a b : (a | - b) -> (a | b).a, b:Z
(a | - b) -> (a | b)
Proof.a, b:Z
(a | - b) -> (a | b) apply Z.divide_opp_r. Qed.

Lemma Zdivide_opp_l a b : (a | b) -> (- a | b).a, b:Z
(a | b) -> (- a | b)
Proof.a, b:Z
(a | b) -> (- a | b) apply Z.divide_opp_l. Qed.

Lemma Zdivide_opp_l_rev a b : (- a | b) -> (a | b).a, b:Z
(- a | b) -> (a | b)
Proof.a, b:Z
(- a | b) -> (a | b) apply Z.divide_opp_l. Qed.

Theorem Zdivide_Zabs_l a b : (Z.abs a | b) -> (a | b).a, b:Z
(Z.abs a | b) -> (a | b)
Proof.a, b:Z
(Z.abs a | b) -> (a | b) apply Z.divide_abs_l. Qed.

Theorem Zdivide_Zabs_inv_l a b : (a | b) -> (Z.abs a | b).a, b:Z
(a | b) -> (Z.abs a | b)
Proof.a, b:Z
(a | b) -> (Z.abs a | b) apply Z.divide_abs_l. Qed.

Hint Resolve Z.divide_refl Z.divide_1_l Z.divide_0_r: zarith.
Hint Resolve Z.mul_divide_mono_l Z.mul_divide_mono_r: zarith.
Hint Resolve Z.divide_add_r Zdivide_opp_r Zdivide_opp_r_rev Zdivide_opp_l
  Zdivide_opp_l_rev Z.divide_sub_r Z.divide_mul_l Z.divide_mul_r
  Z.divide_factor_l Z.divide_factor_r: zarith.

Auxiliary result.

Lemma Zmult_one x y : x >= 0 -> x * y = 1 -> x = 1.x, y:Z
x >= 0 -> x * y = 1 -> x = 1
Proof.x, y:Z
x >= 0 -> x * y = 1 -> x = 1
 Z.swap_greater.x, y:Z
0 <= x -> x * y = 1 -> x = 1 apply Z.eq_mul_1_nonneg.
Qed.

Only 1 and -1 divide 1.

Notation Zdivide_1 := Z.divide_1_r (only parsing).

If a divides b and b<>0 then |a| ≤ |b|.

Lemma Zdivide_bounds a b : (a | b) -> b <> 0 -> Z.abs a <= Z.abs b.a, b:Z
(a | b) -> b <> 0 -> Z.abs a <= Z.abs b
Proof.a, b:Z
(a | b) -> b <> 0 -> Z.abs a <= Z.abs b
 intros H Hb.a, b:Z
H:(a | b)
Hb:b <> 0
Z.abs a <= Z.abs b
 rewrite <- Z.divide_abs_l, <- Z.divide_abs_r in H.a, b:Z
H:(Z.abs a | Z.abs b)
Hb:b <> 0
Z.abs a <= Z.abs b
 apply Z.abs_pos in Hb.a, b:Z
H:(Z.abs a | Z.abs b)
Hb:0 < Z.abs b
Z.abs a <= Z.abs b
 now apply Z.divide_pos_le.
Qed.

Z.divide can be expressed using Z.modulo.

Lemma Zmod_divide : forall a b, b<>0 -> a mod b = 0 -> (b | a).forall a b : Z, b <> 0 -> a mod b = 0 -> (b | a)
Proof.forall a b : Z, b <> 0 -> a mod b = 0 -> (b | a)
 apply Z.mod_divide.
Qed.

Lemma Zdivide_mod : forall a b, (b | a) -> a mod b = 0.forall a b : Z, (b | a) -> a mod b = 0
Proof.forall a b : Z, (b | a) -> a mod b = 0
 intros a b (c,->); apply Z_mod_mult.
Qed.

Z.divide is hence decidable

Lemma Zdivide_dec a b : {(a | b)} + {~ (a | b)}.a, b:Z
{(a | b)} + {~ (a | b)}
Proof.a, b:Z
{(a | b)} + {~ (a | b)}
 destruct (Z.eq_dec a 0) as [Ha|Ha].a, b:Z
Ha:a = 0
{(a | b)} + {~ (a | b)}
a, b:Z
Ha:a <> 0
{(a | b)} + {~ (a | b)}
  destruct (Z.eq_dec b 0) as [Hb|Hb].a, b:Z
Ha:a = 0
Hb:b = 0
{(a | b)} + {~ (a | b)}
a, b:Z
Ha:a = 0
Hb:b <> 0
{(a | b)} + {~ (a | b)}
a, b:Z
Ha:a <> 0
{(a | b)} + {~ (a | b)}
   left; subst; apply Z.divide_0_r.a, b:Z
Ha:a = 0
Hb:b <> 0
{(a | b)} + {~ (a | b)}
a, b:Z
Ha:a <> 0
{(a | b)} + {~ (a | b)}
   right.a, b:Z
Ha:a = 0
Hb:b <> 0
~ (a | b)
a, b:Z
Ha:a <> 0
{(a | b)} + {~ (a | b)} subst.b:Z
Hb:b <> 0
~ (0 | b)
a, b:Z
Ha:a <> 0
{(a | b)} + {~ (a | b)} contradict Hb.b:Z
Hb:(0 | b)
b = 0
a, b:Z
Ha:a <> 0
{(a | b)} + {~ (a | b)} now apply Z.divide_0_l.a, b:Z
Ha:a <> 0
{(a | b)} + {~ (a | b)}
  destruct (Z.eq_dec (b mod a) 0).a, b:Z
Ha:a <> 0
e:b mod a = 0
{(a | b)} + {~ (a | b)}
a, b:Z
Ha:a <> 0
n:b mod a <> 0
{(a | b)} + {~ (a | b)}
   left.a, b:Z
Ha:a <> 0
e:b mod a = 0
(a | b)
a, b:Z
Ha:a <> 0
n:b mod a <> 0
{(a | b)} + {~ (a | b)} now apply Z.mod_divide.a, b:Z
Ha:a <> 0
n:b mod a <> 0
{(a | b)} + {~ (a | b)}
   right.a, b:Z
Ha:a <> 0
n:b mod a <> 0
~ (a | b) now rewrite <- Z.mod_divide.
Defined.

Theorem Zdivide_Zdiv_eq a b : 0 < a -> (a | b) ->  b = a * (b / a).a, b:Z
0 < a -> (a | b) -> b = a * (b / a)
Proof.a, b:Z
0 < a -> (a | b) -> b = a * (b / a)
 intros Ha H.a, b:Z
Ha:0 < a
H:(a | b)
b = a * (b / a)
 rewrite (Z.div_mod b a) at 1; auto with zarith.a, b:Z
Ha:0 < a
H:(a | b)
a * (b / a) + b mod a = a * (b / a)
 rewrite Zdivide_mod; auto with zarith.
Qed.

Theorem Zdivide_Zdiv_eq_2 a b c :
 0 < a -> (a | b) -> (c * b) / a = c * (b / a).a, b, c:Z
0 < a -> (a | b) -> c * b / a = c * (b / a)
Proof.a, b, c:Z
0 < a -> (a | b) -> c * b / a = c * (b / a)
 intros.a, b, c:Z
H:0 < a
H0:(a | b)
c * b / a = c * (b / a) apply Z.divide_div_mul_exact; auto with zarith.
Qed.

Theorem Zdivide_le: forall a b : Z,
 0 <= a -> 0 < b -> (a | b) ->  a <= b.forall a b : Z, 0 <= a -> 0 < b -> (a | b) -> a <= b
Proof.forall a b : Z, 0 <= a -> 0 < b -> (a | b) -> a <= b
 intros.a, b:Z
H:0 <= a
H0:0 < b
H1:(a | b)
a <= b now apply Z.divide_pos_le.
Qed.

Theorem Zdivide_Zdiv_lt_pos a b :
 1 < a -> 0 < b -> (a | b) ->  0 < b / a < b .a, b:Z
1 < a -> 0 < b -> (a | b) -> 0 < b / a < b
Proof.a, b:Z
1 < a -> 0 < b -> (a | b) -> 0 < b / a < b
  intros H1 H2 H3; split.a, b:Z
H1:1 < a
H2:0 < b
H3:(a | b)
0 < b / a
a, b:Z
H1:1 < a
H2:0 < b
H3:(a | b)
b / a < b
  apply Z.mul_pos_cancel_l with a; auto with zarith.a, b:Z
H1:1 < a
H2:0 < b
H3:(a | b)
0 < a * (b / a)
a, b:Z
H1:1 < a
H2:0 < b
H3:(a | b)
b / a < b
  rewrite <- Zdivide_Zdiv_eq; auto with zarith.a, b:Z
H1:1 < a
H2:0 < b
H3:(a | b)
b / a < b
  now apply Z.div_lt.
Qed.

Lemma Zmod_div_mod n m a:
 0 < n -> 0 < m -> (n | m) -> a mod n = (a mod m) mod n.n, m, a:Z
0 < n -> 0 < m -> (n | m) -> a mod n = (a mod m) mod n
Proof.n, m, a:Z
0 < n -> 0 < m -> (n | m) -> a mod n = (a mod m) mod n
  intros H1 H2 (p,Hp).n, m, a:Z
H1:0 < n
H2:0 < m
p:Z
Hp:m = p * n
a mod n = (a mod m) mod n
  rewrite (Z.div_mod a m) at 1; auto with zarith.n, m, a:Z
H1:0 < n
H2:0 < m
p:Z
Hp:m = p * n
(m * (a / m) + a mod m) mod n = (a mod m) mod n
  rewrite Hp at 1.n, m, a:Z
H1:0 < n
H2:0 < m
p:Z
Hp:m = p * n
(p * n * (a / m) + a mod m) mod n = (a mod m) mod n
  rewrite Z.mul_shuffle0, Z.add_comm, Z.mod_add; auto with zarith.
Qed.

Lemma Zmod_divide_minus a b c:
 0 < b -> a mod b = c -> (b | a - c).a, b, c:Z
0 < b -> a mod b = c -> (b | a - c)
Proof.a, b, c:Z
0 < b -> a mod b = c -> (b | a - c)
  intros H H1.a, b, c:Z
H:0 < b
H1:a mod b = c
(b | a - c) apply Z.mod_divide; auto with zarith.a, b, c:Z
H:0 < b
H1:a mod b = c
(a - c) mod b = 0
  rewrite Zminus_mod; auto with zarith.a, b, c:Z
H:0 < b
H1:a mod b = c
(a mod b - c mod b) mod b = 0
  rewrite H1.a, b, c:Z
H:0 < b
H1:a mod b = c
(c - c mod b) mod b = 0 rewrite <- (Z.mod_small c b) at 1.a, b, c:Z
H:0 < b
H1:a mod b = c
(c mod b - c mod b) mod b = 0
a, b, c:Z
H:0 < b
H1:a mod b = c
0 <= c < b
  rewrite Z.sub_diag, Z.mod_0_l; auto with zarith.a, b, c:Z
H:0 < b
H1:a mod b = c
0 <= c < b
  subst.a, b:Z
H:0 < b
0 <= a mod b < b now apply Z.mod_pos_bound.
Qed.

Lemma Zdivide_mod_minus a b c:
 0 <= c < b -> (b | a - c) -> a mod b = c.a, b, c:Z
0 <= c < b -> (b | a - c) -> a mod b = c
Proof.a, b, c:Z
0 <= c < b -> (b | a - c) -> a mod b = c
  intros (H1, H2) H3.a, b, c:Z
H1:0 <= c
H2:c < b
H3:(b | a - c)
a mod b = c
  assert (0 < b) by Z.order.a, b, c:Z
H1:0 <= c
H2:c < b
H3:(b | a - c)
H:0 < b
a mod b = c
  replace a with ((a - c) + c); auto with zarith.a, b, c:Z
H1:0 <= c
H2:c < b
H3:(b | a - c)
H:0 < b
(a - c + c) mod b = c
  rewrite Z.add_mod; auto with zarith.a, b, c:Z
H1:0 <= c
H2:c < b
H3:(b | a - c)
H:0 < b
((a - c) mod b + c mod b) mod b = c
  rewrite (Zdivide_mod (a-c) b); try rewrite Z.add_0_l; auto with zarith.a, b, c:Z
H1:0 <= c
H2:c < b
H3:(b | a - c)
H:0 < b
(c mod b) mod b = c
  rewrite Z.mod_mod; try apply Zmod_small; auto with zarith.
Qed.

Greatest common divisor (gcd).

There is no unicity of the gcd; hence we define the predicate Zis_gcd a b g expressing that g is a gcd of a and b. (We show later that the gcd is actually unique if we discard its sign.)

Inductive Zis_gcd (a b g:Z) : Prop :=
 Zis_gcd_intro :
  (g | a) ->
  (g | b) ->
  (forall x, (x | a) -> (x | b) -> (x | g)) ->
  Zis_gcd a b g.

Trivial properties of gcd

Lemma Zis_gcd_sym : forall a b d, Zis_gcd a b d -> Zis_gcd b a d.forall a b d : Z, Zis_gcd a b d -> Zis_gcd b a d
Proof.forall a b d : Z, Zis_gcd a b d -> Zis_gcd b a d
  induction 1; constructor; intuition.
Qed.

Lemma Zis_gcd_0 : forall a, Zis_gcd a 0 a.forall a : Z, Zis_gcd a 0 a
Proof.forall a : Z, Zis_gcd a 0 a
  constructor; auto with zarith.
Qed.

Lemma Zis_gcd_1 : forall a, Zis_gcd a 1 1.forall a : Z, Zis_gcd a 1 1
Proof.forall a : Z, Zis_gcd a 1 1
  constructor; auto with zarith.
Qed.

Lemma Zis_gcd_refl : forall a, Zis_gcd a a a.forall a : Z, Zis_gcd a a a
Proof.forall a : Z, Zis_gcd a a a
  constructor; auto with zarith.
Qed.

Lemma Zis_gcd_minus : forall a b d, Zis_gcd a (- b) d -> Zis_gcd b a d.forall a b d : Z, Zis_gcd a (- b) d -> Zis_gcd b a d
Proof.forall a b d : Z, Zis_gcd a (- b) d -> Zis_gcd b a d
  induction 1; constructor; intuition.
Qed.

Lemma Zis_gcd_opp : forall a b d, Zis_gcd a b d -> Zis_gcd b a (- d).forall a b d : Z, Zis_gcd a b d -> Zis_gcd b a (- d)
Proof.forall a b d : Z, Zis_gcd a b d -> Zis_gcd b a (- d)
  induction 1; constructor; intuition.
Qed.

Lemma Zis_gcd_0_abs a : Zis_gcd 0 a (Z.abs a).a:Z
Zis_gcd 0 a (Z.abs a)
Proof.a:Z
Zis_gcd 0 a (Z.abs a)
  apply Zabs_ind.a:Z
a >= 0 -> Zis_gcd 0 a a
a:Z
a <= 0 -> Zis_gcd 0 a (- a)
  intros; apply Zis_gcd_sym; apply Zis_gcd_0; auto.a:Z
a <= 0 -> Zis_gcd 0 a (- a)
  intros; apply Zis_gcd_opp; apply Zis_gcd_0; auto.
Qed.

Hint Resolve Zis_gcd_sym Zis_gcd_0 Zis_gcd_minus Zis_gcd_opp: zarith.

Theorem Zis_gcd_unique: forall a b c d : Z,
 Zis_gcd a b c -> Zis_gcd a b d ->  c = d \/ c = (- d).forall a b c d : Z,
Zis_gcd a b c -> Zis_gcd a b d -> c = d \/ c = - d
Proof.forall a b c d : Z,
Zis_gcd a b c -> Zis_gcd a b d -> c = d \/ c = - d
intros a b c d [Hc1 Hc2 Hc3] [Hd1 Hd2 Hd3].a, b, c, d:Z
Hc1:(c | a)
Hc2:(c | b)
Hc3:forall x : Z, (x | a) -> (x | b) -> (x | c)
Hd1:(d | a)
Hd2:(d | b)
Hd3:forall x : Z, (x | a) -> (x | b) -> (x | d)
c = d \/ c = - d
assert (c|d) by auto.a, b, c, d:Z
Hc1:(c | a)
Hc2:(c | b)
Hc3:forall x : Z, (x | a) -> (x | b) -> (x | c)
Hd1:(d | a)
Hd2:(d | b)
Hd3:forall x : Z, (x | a) -> (x | b) -> (x | d)
H:(c | d)
c = d \/ c = - d
assert (d|c) by auto.a, b, c, d:Z
Hc1:(c | a)
Hc2:(c | b)
Hc3:forall x : Z, (x | a) -> (x | b) -> (x | c)
Hd1:(d | a)
Hd2:(d | b)
Hd3:forall x : Z, (x | a) -> (x | b) -> (x | d)
H:(c | d)
H0:(d | c)
c = d \/ c = - d
apply Z.divide_antisym; auto.
Qed.

Extended Euclid algorithm.

Euclid's algorithm to compute the gcd mainly relies on the following property.

Lemma Zis_gcd_for_euclid :
  forall a b d q:Z, Zis_gcd b (a - q * b) d -> Zis_gcd a b d.forall a b d q : Z,
Zis_gcd b (a - q * b) d -> Zis_gcd a b d
Proof.forall a b d q : Z,
Zis_gcd b (a - q * b) d -> Zis_gcd a b d
  simple induction 1; constructor; intuition.a, b, d, q:Z
H:Zis_gcd b (a - q * b) d
H0:(d | b)
H1:(d | a - q * b)
H2:forall x : Z,
(x | b) -> (x | a - q * b) -> (x | d)
(d | a)
  replace a with (a - q * b + q * b).a, b, d, q:Z
H:Zis_gcd b (a - q * b) d
H0:(d | b)
H1:(d | a - q * b)
H2:forall x : Z,
(x | b) -> (x | a - q * b) -> (x | d)
(d | a - q * b + q * b)
a, b, d, q:Z
H:Zis_gcd b (a - q * b) d
H0:(d | b)
H1:(d | a - q * b)
H2:forall x : Z,
(x | b) -> (x | a - q * b) -> (x | d)
a - q * b + q * b = a auto with zarith.a, b, d, q:Z
H:Zis_gcd b (a - q * b) d
H0:(d | b)
H1:(d | a - q * b)
H2:forall x : Z,
(x | b) -> (x | a - q * b) -> (x | d)
a - q * b + q * b = a ring.
Qed.

Lemma Zis_gcd_for_euclid2 :
  forall b d q r:Z, Zis_gcd r b d -> Zis_gcd b (b * q + r) d.forall b d q r : Z,
Zis_gcd r b d -> Zis_gcd b (b * q + r) d
Proof.forall b d q r : Z,
Zis_gcd r b d -> Zis_gcd b (b * q + r) d
  simple induction 1; constructor; intuition.b, d, q, r:Z
H:Zis_gcd r b d
H0:(d | r)
H1:(d | b)
H2:forall x0 : Z, (x0 | r) -> (x0 | b) -> (x0 | d)
x:Z
H3:(x | b)
H4:(x | b * q + r)
(x | d)
  apply H2; auto.b, d, q, r:Z
H:Zis_gcd r b d
H0:(d | r)
H1:(d | b)
H2:forall x0 : Z, (x0 | r) -> (x0 | b) -> (x0 | d)
x:Z
H3:(x | b)
H4:(x | b * q + r)
(x | r)
  replace r with (b * q + r - b * q).b, d, q, r:Z
H:Zis_gcd r b d
H0:(d | r)
H1:(d | b)
H2:forall x0 : Z, (x0 | r) -> (x0 | b) -> (x0 | d)
x:Z
H3:(x | b)
H4:(x | b * q + r)
(x | b * q + r - b * q)
b, d, q, r:Z
H:Zis_gcd r b d
H0:(d | r)
H1:(d | b)
H2:forall x0 : Z, (x0 | r) -> (x0 | b) -> (x0 | d)
x:Z
H3:(x | b)
H4:(x | b * q + r)
b * q + r - b * q = r auto with zarith.b, d, q, r:Z
H:Zis_gcd r b d
H0:(d | r)
H1:(d | b)
H2:forall x0 : Z, (x0 | r) -> (x0 | b) -> (x0 | d)
x:Z
H3:(x | b)
H4:(x | b * q + r)
b * q + r - b * q = r ring.
Qed.

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.

  Variables 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 :
    forall u v d:Z, u * a + v * b = d -> Zis_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(u3,v3)=gcd(a,b).

  Lemma euclid_rec :
    forall v3:Z,
      0 <= v3 ->
      forall u1 u2 u3 v1 v2:Z,
	u1 * a + u2 * b = u3 ->
	v1 * a + v2 * b = v3 ->
	(forall d:Z, Zis_gcd u3 v3 d -> Zis_gcd a b d) -> Euclid.a, b:Z
forall v3 : Z,
0 <= v3 ->
forall u1 u2 u3 v1 v2 : Z,
u1 * a + u2 * b = u3 ->
v1 * a + v2 * b = v3 ->
(forall d : Z, Zis_gcd u3 v3 d -> Zis_gcd a b d) ->
Euclid
  Proof.a, b:Z
forall v3 : Z,
0 <= v3 ->
forall u1 u2 u3 v1 v2 : Z,
u1 * a + u2 * b = u3 ->
v1 * a + v2 * b = v3 ->
(forall d : Z, Zis_gcd u3 v3 d -> Zis_gcd a b d) ->
Euclid
    intros v3 Hv3; generalize Hv3; pattern v3.a, b, v3:Z
Hv3:0 <= v3
(fun z : Z =>
 0 <= z ->
 forall u1 u2 u3 v1 v2 : Z,
 u1 * a + u2 * b = u3 ->
 v1 * a + v2 * b = z ->
 (forall d : Z, Zis_gcd u3 z d -> Zis_gcd a b d) ->
 Euclid) v3
    apply Zlt_0_rec.a, b, v3:Z
Hv3:0 <= v3
forall x : Z,
(forall y : Z,
 0 <= y < x ->
 0 <= y ->
 forall u1 u2 u3 v1 v2 : Z,
 u1 * a + u2 * b = u3 ->
 v1 * a + v2 * b = y ->
 (forall d : Z, Zis_gcd u3 y d -> Zis_gcd a b d) ->
 Euclid) ->
0 <= x ->
0 <= x ->
forall u1 u2 u3 v1 v2 : Z,
u1 * a + u2 * b = u3 ->
v1 * a + v2 * b = x ->
(forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d) ->
Euclid
a, b, v3:Z
Hv3:0 <= v3
0 <= v3
    clear v3 Hv3; intros.a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Euclid
a, b, v3:Z
Hv3:0 <= v3
0 <= v3
    destruct (Z_zerop x) as [Heq|Hneq].a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Heq:x = 0
Euclid
a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
Euclid
a, b, v3:Z
Hv3:0 <= v3
0 <= v3
    apply Euclid_intro with (u := u1) (v := u2) (d := u3).a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Heq:x = 0
u1 * a + u2 * b = u3
a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Heq:x = 0
Zis_gcd a b u3
a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
Euclid
a, b, v3:Z
Hv3:0 <= v3
0 <= v3
    assumption.a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Heq:x = 0
Zis_gcd a b u3
a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
Euclid
a, b, v3:Z
Hv3:0 <= v3
0 <= v3
    apply H3.a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Heq:x = 0
Zis_gcd u3 x u3
a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
Euclid
a, b, v3:Z
Hv3:0 <= v3
0 <= v3
    rewrite Heq; auto with zarith.a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
Euclid
a, b, v3:Z
Hv3:0 <= v3
0 <= v3
    set (q := u3 / x) in *.a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
q:=u3 / x:Z
Euclid
a, b, v3:Z
Hv3:0 <= v3
0 <= v3
    assert (Hq : 0 <= u3 - q * x < x).a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
q:=u3 / x:Z
0 <= u3 - q * x < x
a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
q:=u3 / x:Z
Hq:0 <= u3 - q * x < x
Euclid
a, b, v3:Z
Hv3:0 <= v3
0 <= v3
    replace (u3 - q * x) with (u3 mod x).a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
q:=u3 / x:Z
0 <= u3 mod x < x
a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
q:=u3 / x:Z
u3 mod x = u3 - q * x
a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
q:=u3 / x:Z
Hq:0 <= u3 - q * x < x
Euclid
a, b, v3:Z
Hv3:0 <= v3
0 <= v3
    apply Z_mod_lt; omega.a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
q:=u3 / x:Z
u3 mod x = u3 - q * x
a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
q:=u3 / x:Z
Hq:0 <= u3 - q * x < x
Euclid
a, b, v3:Z
Hv3:0 <= v3
0 <= v3
    assert (xpos : x > 0).a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
q:=u3 / x:Z
x > 0
a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
q:=u3 / x:Z
xpos:x > 0
u3 mod x = u3 - q * x
a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
q:=u3 / x:Z
Hq:0 <= u3 - q * x < x
Euclid
a, b, v3:Z
Hv3:0 <= v3
0 <= v3 omega.a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
q:=u3 / x:Z
xpos:x > 0
u3 mod x = u3 - q * x
a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
q:=u3 / x:Z
Hq:0 <= u3 - q * x < x
Euclid
a, b, v3:Z
Hv3:0 <= v3
0 <= v3
    generalize (Z_div_mod_eq u3 x xpos).a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
q:=u3 / x:Z
xpos:x > 0
u3 = x * (u3 / x) + u3 mod x -> u3 mod x = u3 - q * x
a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
q:=u3 / x:Z
Hq:0 <= u3 - q * x < x
Euclid
a, b, v3:Z
Hv3:0 <= v3
0 <= v3
    unfold q.a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
q:=u3 / x:Z
xpos:x > 0
u3 = x * (u3 / x) + u3 mod x ->
u3 mod x = u3 - u3 / x * x
a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
q:=u3 / x:Z
Hq:0 <= u3 - q * x < x
Euclid
a, b, v3:Z
Hv3:0 <= v3
0 <= v3
    intro eq; pattern u3 at 2; rewrite eq; ring.a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
q:=u3 / x:Z
Hq:0 <= u3 - q * x < x
Euclid
a, b, v3:Z
Hv3:0 <= v3
0 <= v3
    apply (H (u3 - q * x) Hq (proj1 Hq) v1 v2 x (u1 - q * v1) (u2 - q * v2)).a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
q:=u3 / x:Z
Hq:0 <= u3 - q * x < x
v1 * a + v2 * b = x
a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
q:=u3 / x:Z
Hq:0 <= u3 - q * x < x
(u1 - q * v1) * a + (u2 - q * v2) * b = u3 - q * x
a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
q:=u3 / x:Z
Hq:0 <= u3 - q * x < x
forall d : Z,
Zis_gcd x (u3 - q * x) d -> Zis_gcd a b d
a, b, v3:Z
Hv3:0 <= v3
0 <= v3
    tauto.a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
q:=u3 / x:Z
Hq:0 <= u3 - q * x < x
(u1 - q * v1) * a + (u2 - q * v2) * b = u3 - q * x
a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
q:=u3 / x:Z
Hq:0 <= u3 - q * x < x
forall d : Z,
Zis_gcd x (u3 - q * x) d -> Zis_gcd a b d
a, b, v3:Z
Hv3:0 <= v3
0 <= v3
    replace ((u1 - q * v1) * a + (u2 - q * v2) * b) with
      (u1 * a + u2 * b - q * (v1 * a + v2 * b)).a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
q:=u3 / x:Z
Hq:0 <= u3 - q * x < x
u1 * a + u2 * b - q * (v1 * a + v2 * b) = u3 - q * x
a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
q:=u3 / x:Z
Hq:0 <= u3 - q * x < x
u1 * a + u2 * b - q * (v1 * a + v2 * b) =
(u1 - q * v1) * a + (u2 - q * v2) * b
a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
q:=u3 / x:Z
Hq:0 <= u3 - q * x < x
forall d : Z,
Zis_gcd x (u3 - q * x) d -> Zis_gcd a b d
a, b, v3:Z
Hv3:0 <= v3
0 <= v3
    rewrite H1; rewrite H2; trivial.a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
q:=u3 / x:Z
Hq:0 <= u3 - q * x < x
u1 * a + u2 * b - q * (v1 * a + v2 * b) =
(u1 - q * v1) * a + (u2 - q * v2) * b
a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
q:=u3 / x:Z
Hq:0 <= u3 - q * x < x
forall d : Z,
Zis_gcd x (u3 - q * x) d -> Zis_gcd a b d
a, b, v3:Z
Hv3:0 <= v3
0 <= v3
    ring.a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d : Z, Zis_gcd u5 y d -> Zis_gcd a b d) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d : Z, Zis_gcd u3 x d -> Zis_gcd a b d
Hneq:x <> 0
q:=u3 / x:Z
Hq:0 <= u3 - q * x < x
forall d : Z,
Zis_gcd x (u3 - q * x) d -> Zis_gcd a b d
a, b, v3:Z
Hv3:0 <= v3
0 <= v3
    intros; apply H3.a, b, x:Z
H:forall y : Z,
0 <= y < x ->
0 <= y ->
forall u0 u4 u5 v0 v3 : Z,
u0 * a + u4 * b = u5 ->
v0 * a + v3 * b = y ->
(forall d0 : Z, Zis_gcd u5 y d0 -> Zis_gcd a b d0) ->
Euclid
H0, Hv3:0 <= x
u1, u2, u3, v1, v2:Z
H1:u1 * a + u2 * b = u3
H2:v1 * a + v2 * b = x
H3:forall d0 : Z, Zis_gcd u3 x d0 -> Zis_gcd a b d0
Hneq:x <> 0
q:=u3 / x:Z
Hq:0 <= u3 - q * x < x
d:Z
H4:Zis_gcd x (u3 - q * x) d
Zis_gcd u3 x d
a, b, v3:Z
Hv3:0 <= v3
0 <= v3
    apply Zis_gcd_for_euclid with q; assumption.a, b, v3:Z
Hv3:0 <= v3
0 <= v3
    assumption.
  Qed.

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.a, b:Z
Euclid
  Proof.a, b:Z
Euclid
    case (Z_le_gt_dec 0 b); intro.a, b:Z
l:0 <= b
Euclid
a, b:Z
g:0 > b
Euclid
    intros;
      apply euclid_rec with
	(u1 := 1) (u2 := 0) (u3 := a) (v1 := 0) (v2 := 1) (v3 := b);
	auto with zarith; ring.a, b:Z
g:0 > b
Euclid
    intros;
      apply euclid_rec with
	(u1 := 1) (u2 := 0) (u3 := a) (v1 := 0) (v2 := -1) (v3 := - b);
	auto with zarith; try ring.
  Qed.

End extended_euclid_algorithm.

Theorem Zis_gcd_uniqueness_apart_sign :
  forall a b d d':Z, Zis_gcd a b d -> Zis_gcd a b d' -> d = d' \/ d = - d'.forall a b d d' : Z,
Zis_gcd a b d -> Zis_gcd a b d' -> d = d' \/ d = - d'
Proof.forall a b d d' : Z,
Zis_gcd a b d -> Zis_gcd a b d' -> d = d' \/ d = - d'
  simple induction 1.a, b, d, d':Z
H:Zis_gcd a b d
(d | a) ->
(d | b) ->
(forall x : Z, (x | a) -> (x | b) -> (x | d)) ->
Zis_gcd a b d' -> d = d' \/ d = - d'
  intros H1 H2 H3; simple induction 1; intros.a, b, d, d':Z
H:Zis_gcd a b d
H1:(d | a)
H2:(d | b)
H3:forall x : Z, (x | a) -> (x | b) -> (x | d)
H0:Zis_gcd a b d'
H4:(d' | a)
H5:(d' | b)
H6:forall x : Z, (x | a) -> (x | b) -> (x | d')
d = d' \/ d = - d'
  generalize (H3 d' H4 H5); intro Hd'd.a, b, d, d':Z
H:Zis_gcd a b d
H1:(d | a)
H2:(d | b)
H3:forall x : Z, (x | a) -> (x | b) -> (x | d)
H0:Zis_gcd a b d'
H4:(d' | a)
H5:(d' | b)
H6:forall x : Z, (x | a) -> (x | b) -> (x | d')
Hd'd:(d' | d)
d = d' \/ d = - d'
  generalize (H6 d H1 H2); intro Hdd'.a, b, d, d':Z
H:Zis_gcd a b d
H1:(d | a)
H2:(d | b)
H3:forall x : Z, (x | a) -> (x | b) -> (x | d)
H0:Zis_gcd a b d'
H4:(d' | a)
H5:(d' | b)
H6:forall x : Z, (x | a) -> (x | b) -> (x | d')
Hd'd:(d' | d)
Hdd':(d | d')
d = d' \/ d = - d'
  exact (Z.divide_antisym d d' Hdd' Hd'd).
Qed.

Bezout's coefficients

Inductive Bezout (a b d:Z) : Prop :=
  Bezout_intro : forall 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 Zis_gcd_bezout : forall a b d:Z, Zis_gcd a b d -> Bezout a b d.forall a b d : Z, Zis_gcd a b d -> Bezout a b d
Proof.forall a b d : Z, Zis_gcd a b d -> Bezout a b d
  intros a b d Hgcd.a, b, d:Z
Hgcd:Zis_gcd a b d
Bezout a b d
  elim (euclid a b); intros u v d0 e g.a, b, d:Z
Hgcd:Zis_gcd a b d
u, v, d0:Z
e:u * a + v * b = d0
g:Zis_gcd a b d0
Bezout a b d
  generalize (Zis_gcd_uniqueness_apart_sign a b d d0 Hgcd g).a, b, d:Z
Hgcd:Zis_gcd a b d
u, v, d0:Z
e:u * a + v * b = d0
g:Zis_gcd a b d0
d = d0 \/ d = - d0 -> Bezout a b d
  intro H; elim H; clear H; intros.a, b, d:Z
Hgcd:Zis_gcd a b d
u, v, d0:Z
e:u * a + v * b = d0
g:Zis_gcd a b d0
H:d = d0
Bezout a b d
a, b, d:Z
Hgcd:Zis_gcd a b d
u, v, d0:Z
e:u * a + v * b = d0
g:Zis_gcd a b d0
H:d = - d0
Bezout a b d
  apply Bezout_intro with u v.a, b, d:Z
Hgcd:Zis_gcd a b d
u, v, d0:Z
e:u * a + v * b = d0
g:Zis_gcd a b d0
H:d = d0
u * a + v * b = d
a, b, d:Z
Hgcd:Zis_gcd a b d
u, v, d0:Z
e:u * a + v * b = d0
g:Zis_gcd a b d0
H:d = - d0
Bezout a b d
  rewrite H; assumption.a, b, d:Z
Hgcd:Zis_gcd a b d
u, v, d0:Z
e:u * a + v * b = d0
g:Zis_gcd a b d0
H:d = - d0
Bezout a b d
  apply Bezout_intro with (- u) (- v).a, b, d:Z
Hgcd:Zis_gcd a b d
u, v, d0:Z
e:u * a + v * b = d0
g:Zis_gcd a b d0
H:d = - d0
- u * a + - v * b = d
  rewrite H; rewrite <- e; ring.
Qed.

gcd of ca and cb is c gcd(a,b).

Lemma Zis_gcd_mult :
  forall a b c d:Z, Zis_gcd a b d -> Zis_gcd (c * a) (c * b) (c * d).forall a b c d : Z,
Zis_gcd a b d -> Zis_gcd (c * a) (c * b) (c * d)
Proof.forall a b c d : Z,
Zis_gcd a b d -> Zis_gcd (c * a) (c * b) (c * d)
  intros a b c d; simple induction 1.a, b, c, d:Z
H:Zis_gcd a b d
(d | a) ->
(d | b) ->
(forall x : Z, (x | a) -> (x | b) -> (x | d)) ->
Zis_gcd (c * a) (c * b) (c * d) constructor; auto with zarith.a, b, c, d:Z
H:Zis_gcd a b d
H0:(d | a)
H1:(d | b)
H2:forall x : Z, (x | a) -> (x | b) -> (x | d)
forall x : Z,
(x | c * a) -> (x | c * b) -> (x | c * d)
  intros x Ha Hb.a, b, c, d:Z
H:Zis_gcd a b d
H0:(d | a)
H1:(d | b)
H2:forall x0 : Z, (x0 | a) -> (x0 | b) -> (x0 | d)
x:Z
Ha:(x | c * a)
Hb:(x | c * b)
(x | c * d)
  elim (Zis_gcd_bezout a b d H).a, b, c, d:Z
H:Zis_gcd a b d
H0:(d | a)
H1:(d | b)
H2:forall x0 : Z, (x0 | a) -> (x0 | b) -> (x0 | d)
x:Z
Ha:(x | c * a)
Hb:(x | c * b)
forall u v : Z, u * a + v * b = d -> (x | c * d) intros u v Huv.a, b, c, d:Z
H:Zis_gcd a b d
H0:(d | a)
H1:(d | b)
H2:forall x0 : Z, (x0 | a) -> (x0 | b) -> (x0 | d)
x:Z
Ha:(x | c * a)
Hb:(x | c * b)
u, v:Z
Huv:u * a + v * b = d
(x | c * d)
  elim Ha; intros a' Ha'.a, b, c, d:Z
H:Zis_gcd a b d
H0:(d | a)
H1:(d | b)
H2:forall x0 : Z, (x0 | a) -> (x0 | b) -> (x0 | d)
x:Z
Ha:(x | c * a)
Hb:(x | c * b)
u, v:Z
Huv:u * a + v * b = d
a':Z
Ha':c * a = a' * x
(x | c * d)
  elim Hb; intros b' Hb'.a, b, c, d:Z
H:Zis_gcd a b d
H0:(d | a)
H1:(d | b)
H2:forall x0 : Z, (x0 | a) -> (x0 | b) -> (x0 | d)
x:Z
Ha:(x | c * a)
Hb:(x | c * b)
u, v:Z
Huv:u * a + v * b = d
a':Z
Ha':c * a = a' * x
b':Z
Hb':c * b = b' * x
(x | c * d)
  apply Zdivide_intro with (u * a' + v * b').a, b, c, d:Z
H:Zis_gcd a b d
H0:(d | a)
H1:(d | b)
H2:forall x0 : Z, (x0 | a) -> (x0 | b) -> (x0 | d)
x:Z
Ha:(x | c * a)
Hb:(x | c * b)
u, v:Z
Huv:u * a + v * b = d
a':Z
Ha':c * a = a' * x
b':Z
Hb':c * b = b' * x
c * d = (u * a' + v * b') * x
  rewrite <- Huv.a, b, c, d:Z
H:Zis_gcd a b d
H0:(d | a)
H1:(d | b)
H2:forall x0 : Z, (x0 | a) -> (x0 | b) -> (x0 | d)
x:Z
Ha:(x | c * a)
Hb:(x | c * b)
u, v:Z
Huv:u * a + v * b = d
a':Z
Ha':c * a = a' * x
b':Z
Hb':c * b = b' * x
c * (u * a + v * b) = (u * a' + v * b') * x
  replace (c * (u * a + v * b)) with (u * (c * a) + v * (c * b)).a, b, c, d:Z
H:Zis_gcd a b d
H0:(d | a)
H1:(d | b)
H2:forall x0 : Z, (x0 | a) -> (x0 | b) -> (x0 | d)
x:Z
Ha:(x | c * a)
Hb:(x | c * b)
u, v:Z
Huv:u * a + v * b = d
a':Z
Ha':c * a = a' * x
b':Z
Hb':c * b = b' * x
u * (c * a) + v * (c * b) = (u * a' + v * b') * x
a, b, c, d:Z
H:Zis_gcd a b d
H0:(d | a)
H1:(d | b)
H2:forall x0 : Z, (x0 | a) -> (x0 | b) -> (x0 | d)
x:Z
Ha:(x | c * a)
Hb:(x | c * b)
u, v:Z
Huv:u * a + v * b = d
a':Z
Ha':c * a = a' * x
b':Z
Hb':c * b = b' * x
u * (c * a) + v * (c * b) = c * (u * a + v * b)
  rewrite Ha'; rewrite Hb'; ring.a, b, c, d:Z
H:Zis_gcd a b d
H0:(d | a)
H1:(d | b)
H2:forall x0 : Z, (x0 | a) -> (x0 | b) -> (x0 | d)
x:Z
Ha:(x | c * a)
Hb:(x | c * b)
u, v:Z
Huv:u * a + v * b = d
a':Z
Ha':c * a = a' * x
b':Z
Hb':c * b = b' * x
u * (c * a) + v * (c * b) = c * (u * a + v * b)
  ring.
Qed.

Relative primality

Definition rel_prime (a b:Z) : Prop := Zis_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 : forall a b:Z, rel_prime a b -> Bezout a b 1.forall a b : Z, rel_prime a b -> Bezout a b 1
Proof.forall a b : Z, rel_prime a b -> Bezout a b 1
  intros a b; exact (Zis_gcd_bezout a b 1).
Qed.

Lemma bezout_rel_prime : forall a b:Z, Bezout a b 1 -> rel_prime a b.forall a b : Z, Bezout a b 1 -> rel_prime a b
Proof.forall a b : Z, Bezout a b 1 -> rel_prime a b
  simple induction 1; constructor; auto with zarith.a, b:Z
H:Bezout a b 1
u, v:Z
H0:u * a + v * b = 1
forall x : Z, (x | a) -> (x | b) -> (x | 1)
  intros.a, b:Z
H:Bezout a b 1
u, v:Z
H0:u * a + v * b = 1
x:Z
H1:(x | a)
H2:(x | b)
(x | 1) rewrite <- H0; auto with zarith.
Qed.

Gauss's theorem: if a divides bc and if a and b are relatively prime, then a divides c.

Theorem Gauss : forall a b c:Z, (a | b * c) -> rel_prime a b -> (a | c).forall a b c : Z,
(a | b * c) -> rel_prime a b -> (a | c)
Proof.forall a b c : Z,
(a | b * c) -> rel_prime a b -> (a | c)
  intros.a, b, c:Z
H:(a | b * c)
H0:rel_prime a b
(a | c) elim (rel_prime_bezout a b H0); intros.a, b, c:Z
H:(a | b * c)
H0:rel_prime a b
u, v:Z
H1:u * a + v * b = 1
(a | c)
  replace c with (c * 1); [ idtac | ring ].a, b, c:Z
H:(a | b * c)
H0:rel_prime a b
u, v:Z
H1:u * a + v * b = 1
(a | c * 1)
  rewrite <- H1.a, b, c:Z
H:(a | b * c)
H0:rel_prime a b
u, v:Z
H1:u * a + v * b = 1
(a | c * (u * a + v * b))
  replace (c * (u * a + v * b)) with (c * u * a + v * (b * c));
    [ eauto with zarith | ring ].
Qed.

If a is relatively prime to b and c, then it is to bc

Lemma rel_prime_mult :
  forall a b c:Z, rel_prime a b -> rel_prime a c -> rel_prime a (b * c).forall a b c : Z,
rel_prime a b -> rel_prime a c -> rel_prime a (b * c)
Proof.forall a b c : Z,
rel_prime a b -> rel_prime a c -> rel_prime a (b * c)
  intros a b c Hb Hc.a, b, c:Z
Hb:rel_prime a b
Hc:rel_prime a c
rel_prime a (b * c)
  elim (rel_prime_bezout a b Hb); intros.a, b, c:Z
Hb:rel_prime a b
Hc:rel_prime a c
u, v:Z
H:u * a + v * b = 1
rel_prime a (b * c)
  elim (rel_prime_bezout a c Hc); intros.a, b, c:Z
Hb:rel_prime a b
Hc:rel_prime a c
u, v:Z
H:u * a + v * b = 1
u0, v0:Z
H0:u0 * a + v0 * c = 1
rel_prime a (b * c)
  apply bezout_rel_prime.a, b, c:Z
Hb:rel_prime a b
Hc:rel_prime a c
u, v:Z
H:u * a + v * b = 1
u0, v0:Z
H0:u0 * a + v0 * c = 1
Bezout a (b * c) 1
  apply Bezout_intro with
    (u := u * u0 * a + v0 * c * u + u0 * v * b) (v := v * v0).a, b, c:Z
Hb:rel_prime a b
Hc:rel_prime a c
u, v:Z
H:u * a + v * b = 1
u0, v0:Z
H0:u0 * a + v0 * c = 1
(u * u0 * a + v0 * c * u + u0 * v * b) * a +
v * v0 * (b * c) = 1
  rewrite <- H.a, b, c:Z
Hb:rel_prime a b
Hc:rel_prime a c
u, v:Z
H:u * a + v * b = 1
u0, v0:Z
H0:u0 * a + v0 * c = 1
(u * u0 * a + v0 * c * u + u0 * v * b) * a +
v * v0 * (b * c) = u * a + v * b
  replace (u * a + v * b) with ((u * a + v * b) * 1); [ idtac | ring ].a, b, c:Z
Hb:rel_prime a b
Hc:rel_prime a c
u, v:Z
H:u * a + v * b = 1
u0, v0:Z
H0:u0 * a + v0 * c = 1
(u * u0 * a + v0 * c * u + u0 * v * b) * a +
v * v0 * (b * c) = (u * a + v * b) * 1
  rewrite <- H0.a, b, c:Z
Hb:rel_prime a b
Hc:rel_prime a c
u, v:Z
H:u * a + v * b = 1
u0, v0:Z
H0:u0 * a + v0 * c = 1
(u * u0 * a + v0 * c * u + u0 * v * b) * a +
v * v0 * (b * c) = (u * a + v * b) * (u0 * a + v0 * c)
  ring.
Qed.

Lemma rel_prime_cross_prod :
  forall 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.forall 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.forall 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
  intros a b c d; intros.a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
a = c /\ b = d
  elim (Z.divide_antisym b d).a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
b = d -> a = c /\ b = d
a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
b = - d -> a = c /\ b = d
a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
(b | d)
a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
(d | b)
  split; auto with zarith.a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
H4:b = d
a = c
a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
b = - d -> a = c /\ b = d
a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
(b | d)
a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
(d | b)
  rewrite H4 in H3.a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = d * c
H4:b = d
a = c
a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
b = - d -> a = c /\ b = d
a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
(b | d)
a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
(d | b)
  rewrite Z.mul_comm in H3.a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:d * a = d * c
H4:b = d
a = c
a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
b = - d -> a = c /\ b = d
a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
(b | d)
a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
(d | b)
  apply Z.mul_reg_l with d; auto with zarith.a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
b = - d -> a = c /\ b = d
a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
(b | d)
a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
(d | b)
  intros; omega.a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
(b | d)
a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
(d | b)
  apply Gauss with a.a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
(b | a * d)
a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
rel_prime b a
a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
(d | b)
  rewrite H3.a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
(b | b * c)
a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
rel_prime b a
a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
(d | b)
  auto with zarith.a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
rel_prime b a
a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
(d | b)
  red; auto with zarith.a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
(d | b)
  apply Gauss with c.a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
(d | c * b)
a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
rel_prime d c
  rewrite Z.mul_comm.a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
(d | b * c)
a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
rel_prime d c
  rewrite <- H3.a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
(d | a * d)
a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
rel_prime d c
  auto with zarith.a, b, c, d:Z
H:rel_prime a b
H0:rel_prime c d
H1:b > 0
H2:d > 0
H3:a * d = b * c
rel_prime d c
  red; auto with zarith.
Qed.

After factorization by a gcd, the original numbers are relatively prime.

Lemma Zis_gcd_rel_prime :
  forall a b g:Z,
    b > 0 -> g >= 0 -> Zis_gcd a b g -> rel_prime (a / g) (b / g).forall a b g : Z,
b > 0 ->
g >= 0 -> Zis_gcd a b g -> rel_prime (a / g) (b / g)
Proof.forall a b g : Z,
b > 0 ->
g >= 0 -> Zis_gcd a b g -> rel_prime (a / g) (b / g)
  intros a b g; intros.a, b, g:Z
H:b > 0
H0:g >= 0
H1:Zis_gcd a b g
rel_prime (a / g) (b / g)
  assert (g <> 0).a, b, g:Z
H:b > 0
H0:g >= 0
H1:Zis_gcd a b g
g <> 0
a, b, g:Z
H:b > 0
H0:g >= 0
H1:Zis_gcd a b g
H2:g <> 0
rel_prime (a / g) (b / g)
  intro.a, b, g:Z
H:b > 0
H0:g >= 0
H1:Zis_gcd a b g
H2:g = 0
False
a, b, g:Z
H:b > 0
H0:g >= 0
H1:Zis_gcd a b g
H2:g <> 0
rel_prime (a / g) (b / g)
  elim H1; intros.a, b, g:Z
H:b > 0
H0:g >= 0
H1:Zis_gcd a b g
H2:g = 0
H3:(g | a)
H4:(g | b)
H5:forall x : Z, (x | a) -> (x | b) -> (x | g)
False
a, b, g:Z
H:b > 0
H0:g >= 0
H1:Zis_gcd a b g
H2:g <> 0
rel_prime (a / g) (b / g)
  elim H4; intros.a, b, g:Z
H:b > 0
H0:g >= 0
H1:Zis_gcd a b g
H2:g = 0
H3:(g | a)
H4:(g | b)
H5:forall x0 : Z, (x0 | a) -> (x0 | b) -> (x0 | g)
x:Z
H6:b = x * g
False
a, b, g:Z
H:b > 0
H0:g >= 0
H1:Zis_gcd a b g
H2:g <> 0
rel_prime (a / g) (b / g)
  rewrite H2 in H6; subst b; omega.a, b, g:Z
H:b > 0
H0:g >= 0
H1:Zis_gcd a b g
H2:g <> 0
rel_prime (a / g) (b / g)
  unfold rel_prime.a, b, g:Z
H:b > 0
H0:g >= 0
H1:Zis_gcd a b g
H2:g <> 0
Zis_gcd (a / g) (b / g) 1
  destruct H1.a, b, g:Z
H:b > 0
H0:g >= 0
H1:(g | a)
H3:(g | b)
H4:forall x : Z, (x | a) -> (x | b) -> (x | g)
H2:g <> 0
Zis_gcd (a / g) (b / g) 1
  destruct H1 as (a',H1).a, b, g:Z
H:b > 0
H0:g >= 0
a':Z
H1:a = a' * g
H3:(g | b)
H4:forall x : Z, (x | a) -> (x | b) -> (x | g)
H2:g <> 0
Zis_gcd (a / g) (b / g) 1
  destruct H3 as (b',H3).a, b, g:Z
H:b > 0
H0:g >= 0
a':Z
H1:a = a' * g
b':Z
H3:b = b' * g
H4:forall x : Z, (x | a) -> (x | b) -> (x | g)
H2:g <> 0
Zis_gcd (a / g) (b / g) 1
  replace (a/g) with a';
    [|rewrite H1; rewrite Z_div_mult; auto with zarith].a, b, g:Z
H:b > 0
H0:g >= 0
a':Z
H1:a = a' * g
b':Z
H3:b = b' * g
H4:forall x : Z, (x | a) -> (x | b) -> (x | g)
H2:g <> 0
Zis_gcd a' (b / g) 1
  replace (b/g) with b';
    [|rewrite H3; rewrite Z_div_mult; auto with zarith].a, b, g:Z
H:b > 0
H0:g >= 0
a':Z
H1:a = a' * g
b':Z
H3:b = b' * g
H4:forall x : Z, (x | a) -> (x | b) -> (x | g)
H2:g <> 0
Zis_gcd a' b' 1
  constructor.a, b, g:Z
H:b > 0
H0:g >= 0
a':Z
H1:a = a' * g
b':Z
H3:b = b' * g
H4:forall x : Z, (x | a) -> (x | b) -> (x | g)
H2:g <> 0
(1 | a')
a, b, g:Z
H:b > 0
H0:g >= 0
a':Z
H1:a = a' * g
b':Z
H3:b = b' * g
H4:forall x : Z, (x | a) -> (x | b) -> (x | g)
H2:g <> 0
(1 | b')
a, b, g:Z
H:b > 0
H0:g >= 0
a':Z
H1:a = a' * g
b':Z
H3:b = b' * g
H4:forall x : Z, (x | a) -> (x | b) -> (x | g)
H2:g <> 0
forall x : Z, (x | a') -> (x | b') -> (x | 1)
  exists a'; auto with zarith.a, b, g:Z
H:b > 0
H0:g >= 0
a':Z
H1:a = a' * g
b':Z
H3:b = b' * g
H4:forall x : Z, (x | a) -> (x | b) -> (x | g)
H2:g <> 0
(1 | b')
a, b, g:Z
H:b > 0
H0:g >= 0
a':Z
H1:a = a' * g
b':Z
H3:b = b' * g
H4:forall x : Z, (x | a) -> (x | b) -> (x | g)
H2:g <> 0
forall x : Z, (x | a') -> (x | b') -> (x | 1)
  exists b'; auto with zarith.a, b, g:Z
H:b > 0
H0:g >= 0
a':Z
H1:a = a' * g
b':Z
H3:b = b' * g
H4:forall x : Z, (x | a) -> (x | b) -> (x | g)
H2:g <> 0
forall x : Z, (x | a') -> (x | b') -> (x | 1)
  intros x (xa,H5) (xb,H6).a, b, g:Z
H:b > 0
H0:g >= 0
a':Z
H1:a = a' * g
b':Z
H3:b = b' * g
H4:forall x0 : Z, (x0 | a) -> (x0 | b) -> (x0 | g)
H2:g <> 0
x, xa:Z
H5:a' = xa * x
xb:Z
H6:b' = xb * x
(x | 1)
  destruct (H4 (x*g)) as (x',Hx').a, b, g:Z
H:b > 0
H0:g >= 0
a':Z
H1:a = a' * g
b':Z
H3:b = b' * g
H4:forall x0 : Z, (x0 | a) -> (x0 | b) -> (x0 | g)
H2:g <> 0
x, xa:Z
H5:a' = xa * x
xb:Z
H6:b' = xb * x
(x * g | a)
a, b, g:Z
H:b > 0
H0:g >= 0
a':Z
H1:a = a' * g
b':Z
H3:b = b' * g
H4:forall x0 : Z, (x0 | a) -> (x0 | b) -> (x0 | g)
H2:g <> 0
x, xa:Z
H5:a' = xa * x
xb:Z
H6:b' = xb * x
(x * g | b)
a, b, g:Z
H:b > 0
H0:g >= 0
a':Z
H1:a = a' * g
b':Z
H3:b = b' * g
H4:forall x0 : Z, (x0 | a) -> (x0 | b) -> (x0 | g)
H2:g <> 0
x, xa:Z
H5:a' = xa * x
xb:Z
H6:b' = xb * x
x':Z
Hx':g = x' * (x * g)
(x | 1)
  exists xa; rewrite Z.mul_assoc; rewrite <- H5; auto.a, b, g:Z
H:b > 0
H0:g >= 0
a':Z
H1:a = a' * g
b':Z
H3:b = b' * g
H4:forall x0 : Z, (x0 | a) -> (x0 | b) -> (x0 | g)
H2:g <> 0
x, xa:Z
H5:a' = xa * x
xb:Z
H6:b' = xb * x
(x * g | b)
a, b, g:Z
H:b > 0
H0:g >= 0
a':Z
H1:a = a' * g
b':Z
H3:b = b' * g
H4:forall x0 : Z, (x0 | a) -> (x0 | b) -> (x0 | g)
H2:g <> 0
x, xa:Z
H5:a' = xa * x
xb:Z
H6:b' = xb * x
x':Z
Hx':g = x' * (x * g)
(x | 1)
  exists xb; rewrite Z.mul_assoc; rewrite <- H6; auto.a, b, g:Z
H:b > 0
H0:g >= 0
a':Z
H1:a = a' * g
b':Z
H3:b = b' * g
H4:forall x0 : Z, (x0 | a) -> (x0 | b) -> (x0 | g)
H2:g <> 0
x, xa:Z
H5:a' = xa * x
xb:Z
H6:b' = xb * x
x':Z
Hx':g = x' * (x * g)
(x | 1)
  replace g with (1*g) in Hx'; auto with zarith.a, b, g:Z
H:b > 0
H0:g >= 0
a':Z
H1:a = a' * g
b':Z
H3:b = b' * g
H4:forall x0 : Z, (x0 | a) -> (x0 | b) -> (x0 | g)
H2:g <> 0
x, xa:Z
H5:a' = xa * x
xb:Z
H6:b' = xb * x
x':Z
Hx':1 * g = x' * (x * (1 * g))
(x | 1)
  do 2 rewrite Z.mul_assoc in Hx'.a, b, g:Z
H:b > 0
H0:g >= 0
a':Z
H1:a = a' * g
b':Z
H3:b = b' * g
H4:forall x0 : Z, (x0 | a) -> (x0 | b) -> (x0 | g)
H2:g <> 0
x, xa:Z
H5:a' = xa * x
xb:Z
H6:b' = xb * x
x':Z
Hx':1 * g = x' * x * 1 * g
(x | 1)
  apply Z.mul_reg_r in Hx'; trivial.a, b, g:Z
H:b > 0
H0:g >= 0
a':Z
H1:a = a' * g
b':Z
H3:b = b' * g
H4:forall x0 : Z, (x0 | a) -> (x0 | b) -> (x0 | g)
H2:g <> 0
x, xa:Z
H5:a' = xa * x
xb:Z
H6:b' = xb * x
x':Z
Hx':1 = x' * x * 1
(x | 1)
  rewrite Z.mul_1_r in Hx'.a, b, g:Z
H:b > 0
H0:g >= 0
a':Z
H1:a = a' * g
b':Z
H3:b = b' * g
H4:forall x0 : Z, (x0 | a) -> (x0 | b) -> (x0 | g)
H2:g <> 0
x, xa:Z
H5:a' = xa * x
xb:Z
H6:b' = xb * x
x':Z
Hx':1 = x' * x
(x | 1)
  exists x'; auto with zarith.
Qed.

Theorem rel_prime_sym: forall a b, rel_prime a b -> rel_prime b a.forall a b : Z, rel_prime a b -> rel_prime b a
Proof.forall a b : Z, rel_prime a b -> rel_prime b a
  intros a b H; auto with zarith.a, b:Z
H:rel_prime a b
rel_prime b a
  red; apply Zis_gcd_sym; auto with zarith.
Qed.

Theorem rel_prime_div: forall p q r,
 rel_prime p q -> (r | p) -> rel_prime r q.forall p q r : Z,
rel_prime p q -> (r | p) -> rel_prime r q
Proof.forall p q r : Z,
rel_prime p q -> (r | p) -> rel_prime r q
  intros p q r H (u, H1); subst.q, r, u:Z
H:rel_prime (u * r) q
rel_prime r q
  inversion_clear H as [H1 H2 H3].q, r, u:Z
H1:(1 | u * r)
H2:(1 | q)
H3:forall x : Z, (x | u * r) -> (x | q) -> (x | 1)
rel_prime r q
  red; apply Zis_gcd_intro; try apply Z.divide_1_l.q, r, u:Z
H1:(1 | u * r)
H2:(1 | q)
H3:forall x : Z, (x | u * r) -> (x | q) -> (x | 1)
forall x : Z, (x | r) -> (x | q) -> (x | 1)
  intros x H4 H5; apply H3; auto.q, r, u:Z
H1:(1 | u * r)
H2:(1 | q)
H3:forall x0 : Z,
(x0 | u * r) -> (x0 | q) -> (x0 | 1)
x:Z
H4:(x | r)
H5:(x | q)
(x | u * r)
  apply Z.divide_mul_r; auto.
Qed.

Theorem rel_prime_1: forall n, rel_prime 1 n.forall n : Z, rel_prime 1 n
Proof.forall n : Z, rel_prime 1 n
  intros n; red; apply Zis_gcd_intro; auto.n:Z
(1 | 1)
n:Z
(1 | n)
  exists 1; auto with zarith.n:Z
(1 | n)
  exists n; auto with zarith.
Qed.

Theorem not_rel_prime_0: forall n, 1 < n -> ~ rel_prime 0 n.forall n : Z, 1 < n -> ~ rel_prime 0 n
Proof.forall n : Z, 1 < n -> ~ rel_prime 0 n
  intros n H H1; absurd (n = 1 \/ n = -1).n:Z
H:1 < n
H1:rel_prime 0 n
~ (n = 1 \/ n = -1)
n:Z
H:1 < n
H1:rel_prime 0 n
n = 1 \/ n = -1
  intros [H2 | H2]; subst; contradict H; auto with zarith.n:Z
H:1 < n
H1:rel_prime 0 n
n = 1 \/ n = -1
  case (Zis_gcd_unique  0 n n 1); auto.n:Z
H:1 < n
H1:rel_prime 0 n
Zis_gcd 0 n n
  apply Zis_gcd_intro; auto.n:Z
H:1 < n
H1:rel_prime 0 n
(n | 0)
n:Z
H:1 < n
H1:rel_prime 0 n
(n | n)
  exists 0; auto with zarith.n:Z
H:1 < n
H1:rel_prime 0 n
(n | n)
  exists 1; auto with zarith.
Qed.

Theorem rel_prime_mod: forall p q, 0 < q ->
 rel_prime p q -> rel_prime (p mod q) q.forall p q : Z,
0 < q -> rel_prime p q -> rel_prime (p mod q) q
Proof.forall p q : Z,
0 < q -> rel_prime p q -> rel_prime (p mod q) q
  intros p q H H0.p, q:Z
H:0 < q
H0:rel_prime p q
rel_prime (p mod q) q
  assert (H1: Bezout p q 1).p, q:Z
H:0 < q
H0:rel_prime p q
Bezout p q 1
p, q:Z
H:0 < q
H0:rel_prime p q
H1:Bezout p q 1
rel_prime (p mod q) q
  apply rel_prime_bezout; auto.p, q:Z
H:0 < q
H0:rel_prime p q
H1:Bezout p q 1
rel_prime (p mod q) q
  inversion_clear H1 as [q1 r1 H2].p, q:Z
H:0 < q
H0:rel_prime p q
q1, r1:Z
H2:q1 * p + r1 * q = 1
rel_prime (p mod q) q
  apply bezout_rel_prime.p, q:Z
H:0 < q
H0:rel_prime p q
q1, r1:Z
H2:q1 * p + r1 * q = 1
Bezout (p mod q) q 1
  apply Bezout_intro with q1  (r1 + q1 * (p / q)).p, q:Z
H:0 < q
H0:rel_prime p q
q1, r1:Z
H2:q1 * p + r1 * q = 1
q1 * (p mod q) + (r1 + q1 * (p / q)) * q = 1
  rewrite <- H2.p, q:Z
H:0 < q
H0:rel_prime p q
q1, r1:Z
H2:q1 * p + r1 * q = 1
q1 * (p mod q) + (r1 + q1 * (p / q)) * q =
q1 * p + r1 * q
  pattern p at 3; rewrite (Z_div_mod_eq p q); try ring; auto with zarith.
Qed.

Theorem rel_prime_mod_rev: forall p q, 0 < q ->
 rel_prime (p mod q) q -> rel_prime p q.forall p q : Z,
0 < q -> rel_prime (p mod q) q -> rel_prime p q
Proof.forall p q : Z,
0 < q -> rel_prime (p mod q) q -> rel_prime p q
  intros p q H H0.p, q:Z
H:0 < q
H0:rel_prime (p mod q) q
rel_prime p q
  rewrite (Z_div_mod_eq p q); auto with zarith; red.p, q:Z
H:0 < q
H0:rel_prime (p mod q) q
Zis_gcd (q * (p / q) + p mod q) q 1
  apply Zis_gcd_sym; apply Zis_gcd_for_euclid2; auto with zarith.
Qed.

Theorem Zrel_prime_neq_mod_0: forall a b, 1 < b -> rel_prime a b -> a mod b <> 0.forall a b : Z, 1 < b -> rel_prime a b -> a mod b <> 0
Proof.forall a b : Z, 1 < b -> rel_prime a b -> a mod b <> 0
  intros a b H H1 H2.a, b:Z
H:1 < b
H1:rel_prime a b
H2:a mod b = 0
False
  case (not_rel_prime_0 _ H).a, b:Z
H:1 < b
H1:rel_prime a b
H2:a mod b = 0
rel_prime 0 b
  rewrite <- H2.a, b:Z
H:1 < b
H1:rel_prime a b
H2:a mod b = 0
rel_prime (a mod b) b
  apply rel_prime_mod; auto with zarith.
Qed.

Primality

Inductive prime (p:Z) : Prop :=
  prime_intro :
    1 < p -> (forall 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 :
  forall p:Z,
    prime p -> forall a:Z, (a | p) -> a = -1 \/ a = 1 \/ a = p \/ a = - p.forall p : Z,
prime p ->
forall a : Z,
(a | p) -> a = -1 \/ a = 1 \/ a = p \/ a = - p
Proof.forall p : Z,
prime p ->
forall a : Z,
(a | p) -> a = -1 \/ a = 1 \/ a = p \/ a = - p
  destruct 1; intros.p:Z
H:1 < p
H0:forall n : Z, 1 <= n < p -> rel_prime n p
a:Z
H1:(a | p)
a = -1 \/ a = 1 \/ a = p \/ a = - p
  assert
    (a = - p \/ - p < a < -1 \/ a = -1 \/ a = 0 \/ a = 1 \/ 1 < a < p \/ a = p).p:Z
H:1 < p
H0:forall n : Z, 1 <= n < p -> rel_prime n p
a:Z
H1:(a | p)
a = - p \/
- p < a < -1 \/
a = -1 \/ a = 0 \/ a = 1 \/ 1 < a < p \/ a = p
p:Z
H:1 < p
H0:forall n : Z, 1 <= n < p -> rel_prime n p
a:Z
H1:(a | p)
H2:a = - p \/
- p < a < -1 \/
a = -1 \/ a = 0 \/ a = 1 \/ 1 < a < p \/ a = p
a = -1 \/ a = 1 \/ a = p \/ a = - p
  {p:Z
H:1 < p
H0:forall n : Z, 1 <= n < p -> rel_prime n p
a:Z
H1:(a | p)
a = - p \/
- p < a < -1 \/
a = -1 \/ a = 0 \/ a = 1 \/ 1 < a < p \/ a = p assert (Z.abs a <= Z.abs p) as H2.p:Z
H:1 < p
H0:forall n : Z, 1 <= n < p -> rel_prime n p
a:Z
H1:(a | p)
Z.abs a <= Z.abs p
p:Z
H:1 < p
H0:forall n : Z, 1 <= n < p -> rel_prime n p
a:Z
H1:(a | p)
H2:Z.abs a <= Z.abs p
a = - p \/
- p < a < -1 \/
a = -1 \/ a = 0 \/ a = 1 \/ 1 < a < p \/ a = p
      apply Zdivide_bounds; [ assumption | omega ].p:Z
H:1 < p
H0:forall n : Z, 1 <= n < p -> rel_prime n p
a:Z
H1:(a | p)
H2:Z.abs a <= Z.abs p
a = - p \/
- p < a < -1 \/
a = -1 \/ a = 0 \/ a = 1 \/ 1 < a < p \/ a = p
    revert H2.p:Z
H:1 < p
H0:forall n : Z, 1 <= n < p -> rel_prime n p
a:Z
H1:(a | p)
Z.abs a <= Z.abs p ->
a = - p \/
- p < a < -1 \/
a = -1 \/ a = 0 \/ a = 1 \/ 1 < a < p \/ a = p
    pattern (Z.abs a); apply Zabs_ind; pattern (Z.abs p); apply Zabs_ind;
    intros; omega. }p:Z
H:1 < p
H0:forall n : Z, 1 <= n < p -> rel_prime n p
a:Z
H1:(a | p)
H2:a = - p \/
- p < a < -1 \/
a = -1 \/ a = 0 \/ a = 1 \/ 1 < a < p \/ a = p
a = -1 \/ a = 1 \/ a = p \/ a = - p
  intuition idtac.p:Z
H:1 < p
H0:forall n : Z, 1 <= n < p -> rel_prime n p
a:Z
H1:(a | p)
H3:- p < a
H4:a < -1
a = -1 \/ a = 1 \/ a = p \/ a = - p
p:Z
H:1 < p
H0:forall n : Z, 1 <= n < p -> rel_prime n p
a:Z
H1:(a | p)
H2:a = 0
a = -1 \/ a = 1 \/ a = p \/ a = - p
p:Z
H:1 < p
H0:forall n : Z, 1 <= n < p -> rel_prime n p
a:Z
H1:(a | p)
H3:1 < a
H4:a < p
a = -1 \/ a = 1 \/ a = p \/ a = - p
  (* -p < a < -1 *)
  -p:Z
H:1 < p
H0:forall n : Z, 1 <= n < p -> rel_prime n p
a:Z
H1:(a | p)
H3:- p < a
H4:a < -1
a = -1 \/ a = 1 \/ a = p \/ a = - p absurd (rel_prime (- a) p); intuition.p:Z
H:1 < p
H0:forall n : Z, 1 <= n < p -> rel_prime n p
a:Z
H1:(a | p)
H3:- p < a
H4:a < -1
H2:rel_prime (- a) p
False
    inversion H2.p:Z
H:1 < p
H0:forall n : Z, 1 <= n < p -> rel_prime n p
a:Z
H1:(a | p)
H3:- p < a
H4:a < -1
H2:rel_prime (- a) p
H5:(1 | - a)
H6:(1 | p)
H7:forall x : Z, (x | - a) -> (x | p) -> (x | 1)
False
    assert (- a | - a) by auto with zarith.p:Z
H:1 < p
H0:forall n : Z, 1 <= n < p -> rel_prime n p
a:Z
H1:(a | p)
H3:- p < a
H4:a < -1
H2:rel_prime (- a) p
H5:(1 | - a)
H6:(1 | p)
H7:forall x : Z, (x | - a) -> (x | p) -> (x | 1)
H8:(- a | - a)
False
    assert (- a | p) by auto with zarith.p:Z
H:1 < p
H0:forall n : Z, 1 <= n < p -> rel_prime n p
a:Z
H1:(a | p)
H3:- p < a
H4:a < -1
H2:rel_prime (- a) p
H5:(1 | - a)
H6:(1 | p)
H7:forall x : Z, (x | - a) -> (x | p) -> (x | 1)
H8:(- a | - a)
H9:(- a | p)
False
    apply H7, Z.divide_1_r in H8; intuition.
  (* a = 0 *)
  -p:Z
H:1 < p
H0:forall n : Z, 1 <= n < p -> rel_prime n p
a:Z
H1:(a | p)
H2:a = 0
a = -1 \/ a = 1 \/ a = p \/ a = - p inversion H1.p:Z
H:1 < p
H0:forall n : Z, 1 <= n < p -> rel_prime n p
a:Z
H1:(a | p)
H2:a = 0
x:Z
H3:p = x * a
a = -1 \/ a = 1 \/ a = p \/ a = - p subst a; omega.
  (* 1 < a < p *)
  -p:Z
H:1 < p
H0:forall n : Z, 1 <= n < p -> rel_prime n p
a:Z
H1:(a | p)
H3:1 < a
H4:a < p
a = -1 \/ a = 1 \/ a = p \/ a = - p absurd (rel_prime a p); intuition.p:Z
H:1 < p
H0:forall n : Z, 1 <= n < p -> rel_prime n p
a:Z
H1:(a | p)
H3:1 < a
H4:a < p
H2:rel_prime a p
False
    inversion H2.p:Z
H:1 < p
H0:forall n : Z, 1 <= n < p -> rel_prime n p
a:Z
H1:(a | p)
H3:1 < a
H4:a < p
H2:rel_prime a p
H5:(1 | a)
H6:(1 | p)
H7:forall x : Z, (x | a) -> (x | p) -> (x | 1)
False
    assert (a | a) by auto with zarith.p:Z
H:1 < p
H0:forall n : Z, 1 <= n < p -> rel_prime n p
a:Z
H1:(a | p)
H3:1 < a
H4:a < p
H2:rel_prime a p
H5:(1 | a)
H6:(1 | p)
H7:forall x : Z, (x | a) -> (x | p) -> (x | 1)
H8:(a | a)
False
    assert (a | p) by auto with zarith.p:Z
H:1 < p
H0:forall n : Z, 1 <= n < p -> rel_prime n p
a:Z
H1:(a | p)
H3:1 < a
H4:a < p
H2:rel_prime a p
H5:(1 | a)
H6:(1 | p)
H7:forall x : Z, (x | a) -> (x | p) -> (x | 1)
H8:(a | a)
H9:(a | p)
False
    apply H7, Z.divide_1_r in H8; intuition.
Qed.

A prime number is relatively prime with any number it does not divide

Lemma prime_rel_prime :
  forall p:Z, prime p -> forall a:Z, ~ (p | a) -> rel_prime p a.forall p : Z,
prime p -> forall a : Z, ~ (p | a) -> rel_prime p a
Proof.forall p : Z,
prime p -> forall a : Z, ~ (p | a) -> rel_prime p a
  intros; constructor; intros; auto with zarith.p:Z
H:prime p
a:Z
H0:~ (p | a)
x:Z
H1:(x | p)
H2:(x | a)
(x | 1)
  apply prime_divisors in H1; intuition; subst; auto with zarith.p:Z
H:prime p
a:Z
H0:(p | a) -> False
H2:(p | a)
(p | 1)
p:Z
H:prime p
a:Z
H0:(p | a) -> False
H2:(- p | a)
(- p | 1)
  -p:Z
H:prime p
a:Z
H0:(p | a) -> False
H2:(p | a)
(p | 1) absurd (p | a); auto with zarith.
  -p:Z
H:prime p
a:Z
H0:(p | a) -> False
H2:(- p | a)
(- p | 1) absurd (p | a); intuition.
Qed.

Hint Resolve prime_rel_prime: zarith.

As a consequence, a prime number is relatively prime with smaller numbers

Theorem rel_prime_le_prime:
 forall a p, prime p -> 1 <=  a < p -> rel_prime a p.forall a p : Z, prime p -> 1 <= a < p -> rel_prime a p
Proof.forall a p : Z, prime p -> 1 <= a < p -> rel_prime a p
  intros a p Hp [H1 H2].a, p:Z
Hp:prime p
H1:1 <= a
H2:a < p
rel_prime a p
  apply rel_prime_sym; apply prime_rel_prime; auto.a, p:Z
Hp:prime p
H1:1 <= a
H2:a < p
~ (p | a)
  intros [q Hq]; subst a.p:Z
Hp:prime p
q:Z
H2:q * p < p
H1:1 <= q * p
False
  case (Z.le_gt_cases q 0); intros Hl.p:Z
Hp:prime p
q:Z
H2:q * p < p
H1:1 <= q * p
Hl:q <= 0
False
p:Z
Hp:prime p
q:Z
H2:q * p < p
H1:1 <= q * p
Hl:0 < q
False
  absurd (q * p <= 0 * p); auto with zarith.p:Z
Hp:prime p
q:Z
H2:q * p < p
H1:1 <= q * p
Hl:0 < q
False
  absurd (1 * p <= q * p); auto with zarith.
Qed.

If a prime p divides ab then it divides either a or b

Lemma prime_mult :
  forall p:Z, prime p -> forall a b:Z, (p | a * b) -> (p | a) \/ (p | b).forall p : Z,
prime p ->
forall a b : Z, (p | a * b) -> (p | a) \/ (p | b)
Proof.forall p : Z,
prime p ->
forall a b : Z, (p | a * b) -> (p | a) \/ (p | b)
  intro p; simple induction 1; intros.p:Z
H:prime p
H0:1 < p
H1:forall n : Z, 1 <= n < p -> rel_prime n p
a, b:Z
H2:(p | a * b)
(p | a) \/ (p | b)
  case (Zdivide_dec p a); intuition.p:Z
H:prime p
H0:1 < p
H1:forall n0 : Z, 1 <= n0 < p -> rel_prime n0 p
a, b:Z
H2:(p | a * b)
n:(p | a) -> False
(p | a) \/ (p | b)
  right; apply Gauss with a; auto with zarith.
Qed.

Lemma not_prime_0: ~ prime 0.~ prime 0
Proof.~ prime 0
  intros H1; case (prime_divisors _ H1 2); auto with zarith.
Qed.

Lemma not_prime_1: ~ prime 1.~ prime 1
Proof.~ prime 1
  intros H1; absurd (1 < 1); auto with zarith.H1:prime 1
1 < 1
  inversion H1; auto.
Qed.

Lemma prime_2: prime 2.prime 2
Proof.prime 2
  apply prime_intro; auto with zarith.forall n : Z, 1 <= n < 2 -> rel_prime n 2
  intros n (H,H'); Z.le_elim H; auto with zarith.n:Z
H:1 < n
H':n < 2
rel_prime n 2
n:Z
H:1 = n
H':n < 2
rel_prime n 2
  -n:Z
H:1 < n
H':n < 2
rel_prime n 2 contradict H'; auto with zarith.
  -n:Z
H:1 = n
H':n < 2
rel_prime n 2 subst n.H':1 < 2
rel_prime 1 2 constructor; auto with zarith.
Qed.

Theorem prime_3: prime 3.prime 3
Proof.prime 3
  apply prime_intro; auto with zarith.forall n : Z, 1 <= n < 3 -> rel_prime n 3
  intros n (H,H'); Z.le_elim H; auto with zarith.n:Z
H:1 < n
H':n < 3
rel_prime n 3
n:Z
H:1 = n
H':n < 3
rel_prime n 3
  -n:Z
H:1 < n
H':n < 3
rel_prime n 3 replace n with 2 by omega.n:Z
H:1 < n
H':n < 3
rel_prime 2 3
    constructor; auto with zarith.n:Z
H:1 < n
H':n < 3
forall x : Z, (x | 2) -> (x | 3) -> (x | 1)
    intros x (q,Hq) (q',Hq').n:Z
H:1 < n
H':n < 3
x, q:Z
Hq:2 = q * x
q':Z
Hq':3 = q' * x
(x | 1)
    exists (q' - q).n:Z
H:1 < n
H':n < 3
x, q:Z
Hq:2 = q * x
q':Z
Hq':3 = q' * x
1 = (q' - q) * x ring_simplify.n:Z
H:1 < n
H':n < 3
x, q:Z
Hq:2 = q * x
q':Z
Hq':3 = q' * x
1 = q' * x - q * x now rewrite <- Hq, <- Hq'.
  -n:Z
H:1 = n
H':n < 3
rel_prime n 3 replace n with 1 by trivial.n:Z
H:1 = n
H':n < 3
rel_prime 1 3
    constructor; auto with zarith.
Qed.

Theorem prime_ge_2 p : prime p ->  2 <= p.p:Z
prime p -> 2 <= p
Proof.p:Z
prime p -> 2 <= p
  intros (Hp,_); auto with zarith.
Qed.

Definition prime' p := 1<p /\ (forall n, 1<n<p -> ~ (n|p)).

Lemma Z_0_1_more x : 0<=x -> x=0 \/ x=1 \/ 1<x.x:Z
0 <= x -> x = 0 \/ x = 1 \/ 1 < x
Proof.x:Z
0 <= x -> x = 0 \/ x = 1 \/ 1 < x
 intros H.x:Z
H:0 <= x
x = 0 \/ x = 1 \/ 1 < x Z.le_elim H; auto.x:Z
H:0 < x
x = 0 \/ x = 1 \/ 1 < x
 apply Z.le_succ_l in H.x:Z
H:Z.succ 0 <= x
x = 0 \/ x = 1 \/ 1 < x change (1 <= x) in H.x:Z
H:1 <= x
x = 0 \/ x = 1 \/ 1 < x Z.le_elim H; auto.
Qed.

Theorem prime_alt p : prime' p <-> prime p.p:Z
prime' p <-> prime p
Proof.p:Z
prime' p <-> prime p
  split; intros (Hp,H).p:Z
Hp:1 < p
H:forall n : Z, 1 < n < p -> ~ (n | p)
prime p
p:Z
Hp:1 < p
H:forall n : Z, 1 <= n < p -> rel_prime n p
prime' p
  - (* prime -> prime' *)p:Z
Hp:1 < p
H:forall n : Z, 1 < n < p -> ~ (n | p)
prime p
    constructor; trivial; intros n Hn.p:Z
Hp:1 < p
H:forall n0 : Z, 1 < n0 < p -> ~ (n0 | p)
n:Z
Hn:1 <= n < p
rel_prime n p
    constructor; auto with zarith; intros x Hxn Hxp.p:Z
Hp:1 < p
H:forall n0 : Z, 1 < n0 < p -> ~ (n0 | p)
n:Z
Hn:1 <= n < p
x:Z
Hxn:(x | n)
Hxp:(x | p)
(x | 1)
    rewrite <- Z.divide_abs_l in Hxn, Hxp |- *.p:Z
Hp:1 < p
H:forall n0 : Z, 1 < n0 < p -> ~ (n0 | p)
n:Z
Hn:1 <= n < p
x:Z
Hxn:(Z.abs x | n)
Hxp:(Z.abs x | p)
(Z.abs x | 1)
    assert (Hx := Z.abs_nonneg x).p:Z
Hp:1 < p
H:forall n0 : Z, 1 < n0 < p -> ~ (n0 | p)
n:Z
Hn:1 <= n < p
x:Z
Hxn:(Z.abs x | n)
Hxp:(Z.abs x | p)
Hx:0 <= Z.abs x
(Z.abs x | 1)
    set (y:=Z.abs x) in *; clearbody y; clear x; rename y into x.p:Z
Hp:1 < p
H:forall n0 : Z, 1 < n0 < p -> ~ (n0 | p)
n:Z
Hn:1 <= n < p
x:Z
Hxn:(x | n)
Hxp:(x | p)
Hx:0 <= x
(x | 1)
    destruct (Z_0_1_more x Hx) as [->|[->|Hx']].p:Z
Hp:1 < p
H:forall n0 : Z, 1 < n0 < p -> ~ (n0 | p)
n:Z
Hn:1 <= n < p
Hx:0 <= 0
Hxp:(0 | p)
Hxn:(0 | n)
(0 | 1)
p:Z
Hp:1 < p
H:forall n0 : Z, 1 < n0 < p -> ~ (n0 | p)
n:Z
Hn:1 <= n < p
Hx:0 <= 1
Hxp:(1 | p)
Hxn:(1 | n)
(1 | 1)
p:Z
Hp:1 < p
H:forall n0 : Z, 1 < n0 < p -> ~ (n0 | p)
n:Z
Hn:1 <= n < p
x:Z
Hxn:(x | n)
Hxp:(x | p)
Hx:0 <= x
Hx':1 < x
(x | 1)
    +p:Z
Hp:1 < p
H:forall n0 : Z, 1 < n0 < p -> ~ (n0 | p)
n:Z
Hn:1 <= n < p
Hx:0 <= 0
Hxp:(0 | p)
Hxn:(0 | n)
(0 | 1) exfalso.p:Z
Hp:1 < p
H:forall n0 : Z, 1 < n0 < p -> ~ (n0 | p)
n:Z
Hn:1 <= n < p
Hx:0 <= 0
Hxp:(0 | p)
Hxn:(0 | n)
False apply Z.divide_0_l in Hxn.p:Z
Hp:1 < p
H:forall n0 : Z, 1 < n0 < p -> ~ (n0 | p)
n:Z
Hn:1 <= n < p
Hx:0 <= 0
Hxp:(0 | p)
Hxn:n = 0
False omega.
    +p:Z
Hp:1 < p
H:forall n0 : Z, 1 < n0 < p -> ~ (n0 | p)
n:Z
Hn:1 <= n < p
Hx:0 <= 1
Hxp:(1 | p)
Hxn:(1 | n)
(1 | 1) now exists 1.
    +p:Z
Hp:1 < p
H:forall n0 : Z, 1 < n0 < p -> ~ (n0 | p)
n:Z
Hn:1 <= n < p
x:Z
Hxn:(x | n)
Hxp:(x | p)
Hx:0 <= x
Hx':1 < x
(x | 1) elim (H x); auto.p:Z
Hp:1 < p
H:forall n0 : Z, 1 < n0 < p -> ~ (n0 | p)
n:Z
Hn:1 <= n < p
x:Z
Hxn:(x | n)
Hxp:(x | p)
Hx:0 <= x
Hx':1 < x
1 < x < p
      split; trivial.p:Z
Hp:1 < p
H:forall n0 : Z, 1 < n0 < p -> ~ (n0 | p)
n:Z
Hn:1 <= n < p
x:Z
Hxn:(x | n)
Hxp:(x | p)
Hx:0 <= x
Hx':1 < x
x < p
      apply Z.le_lt_trans with n; auto with zarith.p:Z
Hp:1 < p
H:forall n0 : Z, 1 < n0 < p -> ~ (n0 | p)
n:Z
Hn:1 <= n < p
x:Z
Hxn:(x | n)
Hxp:(x | p)
Hx:0 <= x
Hx':1 < x
x <= n
      apply Z.divide_pos_le; auto with zarith.
  - (* prime' -> prime *)p:Z
Hp:1 < p
H:forall n : Z, 1 <= n < p -> rel_prime n p
prime' p
    constructor; trivial.p:Z
Hp:1 < p
H:forall n : Z, 1 <= n < p -> rel_prime n p
forall n : Z, 1 < n < p -> ~ (n | p) intros n Hn Hnp.p:Z
Hp:1 < p
H:forall n0 : Z, 1 <= n0 < p -> rel_prime n0 p
n:Z
Hn:1 < n < p
Hnp:(n | p)
False
    case (Zis_gcd_unique n p n 1); auto with zarith.p:Z
Hp:1 < p
H:forall n0 : Z, 1 <= n0 < p -> rel_prime n0 p
n:Z
Hn:1 < n < p
Hnp:(n | p)
Zis_gcd n p n
p:Z
Hp:1 < p
H:forall n0 : Z, 1 <= n0 < p -> rel_prime n0 p
n:Z
Hn:1 < n < p
Hnp:(n | p)
Zis_gcd n p 1
    constructor; auto with zarith.p:Z
Hp:1 < p
H:forall n0 : Z, 1 <= n0 < p -> rel_prime n0 p
n:Z
Hn:1 < n < p
Hnp:(n | p)
Zis_gcd n p 1
    apply H; auto with zarith.
Qed.

Theorem square_not_prime: forall a, ~ prime (a * a).forall a : Z, ~ prime (a * a)
Proof.forall a : Z, ~ prime (a * a)
  intros a Ha.a:Z
Ha:prime (a * a)
False
  rewrite <- (Z.abs_square a) in Ha.a:Z
Ha:prime (Z.abs a * Z.abs a)
False
  assert (H:=Z.abs_nonneg a).a:Z
Ha:prime (Z.abs a * Z.abs a)
H:0 <= Z.abs a
False
  set (b:=Z.abs a) in *; clearbody b; clear a; rename b into a.a:Z
Ha:prime (a * a)
H:0 <= a
False
  rewrite <- prime_alt in Ha; destruct Ha as (Ha,Ha').a:Z
Ha:1 < a * a
Ha':forall n : Z, 1 < n < a * a -> ~ (n | a * a)
H:0 <= a
False
  assert (H' : 1 < a) by now apply (Z.square_lt_simpl_nonneg 1).a:Z
Ha:1 < a * a
Ha':forall n : Z, 1 < n < a * a -> ~ (n | a * a)
H:0 <= a
H':1 < a
False
  apply (Ha' a).a:Z
Ha:1 < a * a
Ha':forall n : Z, 1 < n < a * a -> ~ (n | a * a)
H:0 <= a
H':1 < a
1 < a < a * a
a:Z
Ha:1 < a * a
Ha':forall n : Z, 1 < n < a * a -> ~ (n | a * a)
H:0 <= a
H':1 < a
(a | a * a)
  +a:Z
Ha:1 < a * a
Ha':forall n : Z, 1 < n < a * a -> ~ (n | a * a)
H:0 <= a
H':1 < a
1 < a < a * a split; trivial.a:Z
Ha:1 < a * a
Ha':forall n : Z, 1 < n < a * a -> ~ (n | a * a)
H:0 <= a
H':1 < a
a < a * a
    rewrite <- (Z.mul_1_l a) at 1.a:Z
Ha:1 < a * a
Ha':forall n : Z, 1 < n < a * a -> ~ (n | a * a)
H:0 <= a
H':1 < a
1 * a < a * a apply Z.mul_lt_mono_pos_r; omega.
  +a:Z
Ha:1 < a * a
Ha':forall n : Z, 1 < n < a * a -> ~ (n | a * a)
H:0 <= a
H':1 < a
(a | a * a) exists a; auto.
Qed.

Theorem prime_div_prime: forall p q,
 prime p -> prime q -> (p | q) -> p = q.forall p q : Z, prime p -> prime q -> (p | q) -> p = q
Proof.forall p q : Z, prime p -> prime q -> (p | q) -> p = q
  intros p q H H1 H2;
  assert (Hp: 0 < p); try apply Z.lt_le_trans with 2; try apply prime_ge_2; auto with zarith.p, q:Z
H:prime p
H1:prime q
H2:(p | q)
Hp:0 < p
p = q
  assert (Hq: 0 < q); try apply Z.lt_le_trans with 2; try apply prime_ge_2; auto with zarith.p, q:Z
H:prime p
H1:prime q
H2:(p | q)
Hp:0 < p
Hq:0 < q
p = q
  case prime_divisors with (2 := H2); auto.p, q:Z
H:prime p
H1:prime q
H2:(p | q)
Hp:0 < p
Hq:0 < q
p = -1 -> p = q
p, q:Z
H:prime p
H1:prime q
H2:(p | q)
Hp:0 < p
Hq:0 < q
p = 1 \/ p = q \/ p = - q -> p = q
  intros H4; contradict Hp; subst; auto with zarith.p, q:Z
H:prime p
H1:prime q
H2:(p | q)
Hp:0 < p
Hq:0 < q
p = 1 \/ p = q \/ p = - q -> p = q
  intros [H4| [H4 | H4]]; subst; auto.q:Z
H:prime 1
H1:prime q
Hp:0 < 1
H2:(1 | q)
Hq:0 < q
1 = q
q:Z
H:prime (- q)
H1:prime q
Hp:0 < - q
H2:(- q | q)
Hq:0 < q
- q = q
  contradict H; auto; apply not_prime_1.q:Z
H:prime (- q)
H1:prime q
Hp:0 < - q
H2:(- q | q)
Hq:0 < q
- q = q
  contradict Hp; auto with zarith.
Qed.

we now prove that Z.gcd is indeed a gcd in the sense of Zis_gcd.

Notation Zgcd_is_pos := Z.gcd_nonneg (only parsing).

Lemma Zgcd_is_gcd : forall a b, Zis_gcd a b (Z.gcd a b).forall a b : Z, Zis_gcd a b (Z.gcd a b)
Proof.forall a b : Z, Zis_gcd a b (Z.gcd a b)
 constructor.a, b:Z
(Z.gcd a b | a)
a, b:Z
(Z.gcd a b | b)
a, b:Z
forall x : Z, (x | a) -> (x | b) -> (x | Z.gcd a b)
 apply Z.gcd_divide_l.a, b:Z
(Z.gcd a b | b)
a, b:Z
forall x : Z, (x | a) -> (x | b) -> (x | Z.gcd a b)
 apply Z.gcd_divide_r.a, b:Z
forall x : Z, (x | a) -> (x | b) -> (x | Z.gcd a b)
 apply Z.gcd_greatest.
Qed.

Theorem Zgcd_spec : forall x y : Z, {z : Z | Zis_gcd x y z /\ 0 <= z}.forall x y : Z, {z : Z | Zis_gcd x y z /\ 0 <= z}
Proof.forall x y : Z, {z : Z | Zis_gcd x y z /\ 0 <= z}
  intros x y; exists (Z.gcd x y).x, y:Z
Zis_gcd x y (Z.gcd x y) /\ 0 <= Z.gcd x y
  split; [apply Zgcd_is_gcd  | apply Z.gcd_nonneg].
Qed.

Theorem Zdivide_Zgcd: forall p q r : Z,
 (p | q) -> (p | r) -> (p | Z.gcd q r).forall p q r : Z,
(p | q) -> (p | r) -> (p | Z.gcd q r)
Proof.forall p q r : Z,
(p | q) -> (p | r) -> (p | Z.gcd q r)
 intros.p, q, r:Z
H:(p | q)
H0:(p | r)
(p | Z.gcd q r) now apply Z.gcd_greatest.
Qed.

Theorem Zis_gcd_gcd: forall a b c : Z,
 0 <= c ->  Zis_gcd a b c -> Z.gcd a b = c.forall a b c : Z,
0 <= c -> Zis_gcd a b c -> Z.gcd a b = c
Proof.forall a b c : Z,
0 <= c -> Zis_gcd a b c -> Z.gcd a b = c
  intros a b c H1 H2.a, b, c:Z
H1:0 <= c
H2:Zis_gcd a b c
Z.gcd a b = c
  case (Zis_gcd_uniqueness_apart_sign a b c (Z.gcd a b)); auto.a, b, c:Z
H1:0 <= c
H2:Zis_gcd a b c
Zis_gcd a b (Z.gcd a b)
a, b, c:Z
H1:0 <= c
H2:Zis_gcd a b c
c = - Z.gcd a b -> Z.gcd a b = c
  apply Zgcd_is_gcd; auto.a, b, c:Z
H1:0 <= c
H2:Zis_gcd a b c
c = - Z.gcd a b -> Z.gcd a b = c
  Z.le_elim H1.a, b, c:Z
H1:0 < c
H2:Zis_gcd a b c
c = - Z.gcd a b -> Z.gcd a b = c
a, b, c:Z
H1:0 = c
H2:Zis_gcd a b c
c = - Z.gcd a b -> Z.gcd a b = c
  -a, b, c:Z
H1:0 < c
H2:Zis_gcd a b c
c = - Z.gcd a b -> Z.gcd a b = c generalize (Z.gcd_nonneg a b); auto with zarith.
  -a, b, c:Z
H1:0 = c
H2:Zis_gcd a b c
c = - Z.gcd a b -> Z.gcd a b = c subst.a, b:Z
H2:Zis_gcd a b 0
0 = - Z.gcd a b -> Z.gcd a b = 0 now case (Z.gcd a b).
Qed.

Notation Zgcd_inv_0_l := Z.gcd_eq_0_l (only parsing).
Notation Zgcd_inv_0_r := Z.gcd_eq_0_r (only parsing).

Theorem Zgcd_div_swap0 : forall a b : Z,
 0 < Z.gcd a b ->
 0 < b ->
 (a / Z.gcd a b) * b = a * (b/Z.gcd a b).forall a b : Z,
0 < Z.gcd a b ->
0 < b -> a / Z.gcd a b * b = a * (b / Z.gcd a b)
Proof.forall a b : Z,
0 < Z.gcd a b ->
0 < b -> a / Z.gcd a b * b = a * (b / Z.gcd a b)
  intros a b Hg Hb.a, b:Z
Hg:0 < Z.gcd a b
Hb:0 < b
a / Z.gcd a b * b = a * (b / Z.gcd a b)
  assert (F := Zgcd_is_gcd a b); inversion F as [F1 F2 F3].a, b:Z
Hg:0 < Z.gcd a b
Hb:0 < b
F:Zis_gcd a b (Z.gcd a b)
F1:(Z.gcd a b | a)
F2:(Z.gcd a b | b)
F3:forall x : Z,
(x | a) -> (x | b) -> (x | Z.gcd a b)
a / Z.gcd a b * b = a * (b / Z.gcd a b)
  pattern b at 2; rewrite (Zdivide_Zdiv_eq (Z.gcd a b) b); auto.a, b:Z
Hg:0 < Z.gcd a b
Hb:0 < b
F:Zis_gcd a b (Z.gcd a b)
F1:(Z.gcd a b | a)
F2:(Z.gcd a b | b)
F3:forall x : Z,
(x | a) -> (x | b) -> (x | Z.gcd a b)
a / Z.gcd a b * (Z.gcd a b * (b / Z.gcd a b)) =
a * (b / Z.gcd a b)
  repeat rewrite Z.mul_assoc; f_equal.a, b:Z
Hg:0 < Z.gcd a b
Hb:0 < b
F:Zis_gcd a b (Z.gcd a b)
F1:(Z.gcd a b | a)
F2:(Z.gcd a b | b)
F3:forall x : Z,
(x | a) -> (x | b) -> (x | Z.gcd a b)
a / Z.gcd a b * Z.gcd a b = a
  rewrite Z.mul_comm.a, b:Z
Hg:0 < Z.gcd a b
Hb:0 < b
F:Zis_gcd a b (Z.gcd a b)
F1:(Z.gcd a b | a)
F2:(Z.gcd a b | b)
F3:forall x : Z,
(x | a) -> (x | b) -> (x | Z.gcd a b)
Z.gcd a b * (a / Z.gcd a b) = a
  rewrite <- Zdivide_Zdiv_eq; auto.
Qed.

Theorem Zgcd_div_swap : forall a b c : Z,
 0 < Z.gcd a b ->
 0 < b ->
 (c * a) / Z.gcd a b * b = c * a * (b/Z.gcd a b).forall a b c : Z,
0 < Z.gcd a b ->
0 < b ->
c * a / Z.gcd a b * b = c * a * (b / Z.gcd a b)
Proof.forall a b c : Z,
0 < Z.gcd a b ->
0 < b ->
c * a / Z.gcd a b * b = c * a * (b / Z.gcd a b)
  intros a b c Hg Hb.a, b, c:Z
Hg:0 < Z.gcd a b
Hb:0 < b
c * a / Z.gcd a b * b = c * a * (b / Z.gcd a b)
  assert (F := Zgcd_is_gcd a b); inversion F as [F1 F2 F3].a, b, c:Z
Hg:0 < Z.gcd a b
Hb:0 < b
F:Zis_gcd a b (Z.gcd a b)
F1:(Z.gcd a b | a)
F2:(Z.gcd a b | b)
F3:forall x : Z,
(x | a) -> (x | b) -> (x | Z.gcd a b)
c * a / Z.gcd a b * b = c * a * (b / Z.gcd a b)
  pattern b at 2; rewrite (Zdivide_Zdiv_eq (Z.gcd a b) b); auto.a, b, c:Z
Hg:0 < Z.gcd a b
Hb:0 < b
F:Zis_gcd a b (Z.gcd a b)
F1:(Z.gcd a b | a)
F2:(Z.gcd a b | b)
F3:forall x : Z,
(x | a) -> (x | b) -> (x | Z.gcd a b)
c * a / Z.gcd a b * (Z.gcd a b * (b / Z.gcd a b)) =
c * a * (b / Z.gcd a b)
  repeat rewrite Z.mul_assoc; f_equal.a, b, c:Z
Hg:0 < Z.gcd a b
Hb:0 < b
F:Zis_gcd a b (Z.gcd a b)
F1:(Z.gcd a b | a)
F2:(Z.gcd a b | b)
F3:forall x : Z,
(x | a) -> (x | b) -> (x | Z.gcd a b)
c * a / Z.gcd a b * Z.gcd a b = c * a
  rewrite Zdivide_Zdiv_eq_2; auto.a, b, c:Z
Hg:0 < Z.gcd a b
Hb:0 < b
F:Zis_gcd a b (Z.gcd a b)
F1:(Z.gcd a b | a)
F2:(Z.gcd a b | b)
F3:forall x : Z,
(x | a) -> (x | b) -> (x | Z.gcd a b)
c * (a / Z.gcd a b) * Z.gcd a b = c * a
  repeat rewrite <- Z.mul_assoc; f_equal.a, b, c:Z
Hg:0 < Z.gcd a b
Hb:0 < b
F:Zis_gcd a b (Z.gcd a b)
F1:(Z.gcd a b | a)
F2:(Z.gcd a b | b)
F3:forall x : Z,
(x | a) -> (x | b) -> (x | Z.gcd a b)
a / Z.gcd a b * Z.gcd a b = a
  rewrite Z.mul_comm.a, b, c:Z
Hg:0 < Z.gcd a b
Hb:0 < b
F:Zis_gcd a b (Z.gcd a b)
F1:(Z.gcd a b | a)
F2:(Z.gcd a b | b)
F3:forall x : Z,
(x | a) -> (x | b) -> (x | Z.gcd a b)
Z.gcd a b * (a / Z.gcd a b) = a
  rewrite <- Zdivide_Zdiv_eq; auto.
Qed.

Lemma Zgcd_ass a b c : Z.gcd (Z.gcd a b) c = Z.gcd a (Z.gcd b c).a, b, c:Z
Z.gcd (Z.gcd a b) c = Z.gcd a (Z.gcd b c)
Proof.a, b, c:Z
Z.gcd (Z.gcd a b) c = Z.gcd a (Z.gcd b c)
 symmetry.a, b, c:Z
Z.gcd a (Z.gcd b c) = Z.gcd (Z.gcd a b) c apply Z.gcd_assoc.
Qed.

Notation Zgcd_Zabs := Z.gcd_abs_l (only parsing).
Notation Zgcd_0 := Z.gcd_0_r (only parsing).
Notation Zgcd_1 := Z.gcd_1_r (only parsing).

Hint Resolve Z.gcd_0_r Z.gcd_1_r : zarith.

Theorem Zgcd_1_rel_prime : forall a b,
 Z.gcd a b = 1 <-> rel_prime a b.forall a b : Z, Z.gcd a b = 1 <-> rel_prime a b
Proof.forall a b : Z, Z.gcd a b = 1 <-> rel_prime a b
  unfold rel_prime; split; intro H.a, b:Z
H:Z.gcd a b = 1
Zis_gcd a b 1
a, b:Z
H:Zis_gcd a b 1
Z.gcd a b = 1
  rewrite <- H; apply Zgcd_is_gcd.a, b:Z
H:Zis_gcd a b 1
Z.gcd a b = 1
  case (Zis_gcd_unique a b (Z.gcd a b) 1); auto.a, b:Z
H:Zis_gcd a b 1
Zis_gcd a b (Z.gcd a b)
a, b:Z
H:Zis_gcd a b 1
Z.gcd a b = - (1) -> Z.gcd a b = 1
  apply Zgcd_is_gcd.a, b:Z
H:Zis_gcd a b 1
Z.gcd a b = - (1) -> Z.gcd a b = 1
  intros H2; absurd (0 <= Z.gcd a b); auto with zarith.a, b:Z
H:Zis_gcd a b 1
H2:Z.gcd a b = - (1)
0 <= Z.gcd a b
  generalize (Z.gcd_nonneg a b); auto with zarith.
Qed.

Definition rel_prime_dec: forall a b,
 { rel_prime a b }+{ ~ rel_prime a b }.forall a b : Z, {rel_prime a b} + {~ rel_prime a b}
Proof.forall a b : Z, {rel_prime a b} + {~ rel_prime a b}
  intros a b; case (Z.eq_dec (Z.gcd a b) 1); intros H1.a, b:Z
H1:Z.gcd a b = 1
{rel_prime a b} + {~ rel_prime a b}
a, b:Z
H1:Z.gcd a b <> 1
{rel_prime a b} + {~ rel_prime a b}
  left; apply -> Zgcd_1_rel_prime; auto.a, b:Z
H1:Z.gcd a b <> 1
{rel_prime a b} + {~ rel_prime a b}
  right; contradict H1; apply <- Zgcd_1_rel_prime; auto.
Defined.

Definition prime_dec_aux:
 forall p m,
  { forall n, 1 < n < m -> rel_prime n p } +
  { exists n, 1 < n < m  /\ ~ rel_prime n p }.forall p m : Z,
{forall n : Z, 1 < n < m -> rel_prime n p} +
{exists n : Z, 1 < n < m /\ ~ rel_prime n p}
Proof.forall p m : Z,
{forall n : Z, 1 < n < m -> rel_prime n p} +
{exists n : Z, 1 < n < m /\ ~ rel_prime n p}
  intros p m.p, m:Z
{forall n : Z, 1 < n < m -> rel_prime n p} +
{exists n : Z, 1 < n < m /\ ~ rel_prime n p}
  case (Z_lt_dec 1 m); intros H1;
   [ | left; intros; exfalso; omega ].p, m:Z
H1:1 < m
{forall n : Z, 1 < n < m -> rel_prime n p} +
{exists n : Z, 1 < n < m /\ ~ rel_prime n p}
  pattern m; apply natlike_rec; auto with zarith.p, m:Z
H1:1 < m
{forall n : Z, 1 < n < 0 -> rel_prime n p} +
{exists n : Z, 1 < n < 0 /\ ~ rel_prime n p}
p, m:Z
H1:1 < m
forall x : Z,
0 <= x ->
{forall n : Z, 1 < n < x -> rel_prime n p} +
{exists n : Z, 1 < n < x /\ ~ rel_prime n p} ->
{forall n : Z, 1 < n < Z.succ x -> rel_prime n p} +
{exists n : Z, 1 < n < Z.succ x /\ ~ rel_prime n p}
  left; intros; exfalso; omega.p, m:Z
H1:1 < m
forall x : Z,
0 <= x ->
{forall n : Z, 1 < n < x -> rel_prime n p} +
{exists n : Z, 1 < n < x /\ ~ rel_prime n p} ->
{forall n : Z, 1 < n < Z.succ x -> rel_prime n p} +
{exists n : Z, 1 < n < Z.succ x /\ ~ rel_prime n p}
  intros x Hx IH; destruct IH as [F|E].p, m:Z
H1:1 < m
x:Z
Hx:0 <= x
F:forall n : Z, 1 < n < x -> rel_prime n p
{forall n : Z, 1 < n < Z.succ x -> rel_prime n p} +
{exists n : Z, 1 < n < Z.succ x /\ ~ rel_prime n p}
p, m:Z
H1:1 < m
x:Z
Hx:0 <= x
E:exists n : Z, 1 < n < x /\ ~ rel_prime n p
{forall n : Z, 1 < n < Z.succ x -> rel_prime n p} +
{exists n : Z, 1 < n < Z.succ x /\ ~ rel_prime n p}
  destruct (rel_prime_dec x p) as [Y|N].p, m:Z
H1:1 < m
x:Z
Hx:0 <= x
F:forall n : Z, 1 < n < x -> rel_prime n p
Y:rel_prime x p
{forall n : Z, 1 < n < Z.succ x -> rel_prime n p} +
{exists n : Z, 1 < n < Z.succ x /\ ~ rel_prime n p}
p, m:Z
H1:1 < m
x:Z
Hx:0 <= x
F:forall n : Z, 1 < n < x -> rel_prime n p
N:~ rel_prime x p
{forall n : Z, 1 < n < Z.succ x -> rel_prime n p} +
{exists n : Z, 1 < n < Z.succ x /\ ~ rel_prime n p}
p, m:Z
H1:1 < m
x:Z
Hx:0 <= x
E:exists n : Z, 1 < n < x /\ ~ rel_prime n p
{forall n : Z, 1 < n < Z.succ x -> rel_prime n p} +
{exists n : Z, 1 < n < Z.succ x /\ ~ rel_prime n p}
  left; intros n [HH1 HH2].p, m:Z
H1:1 < m
x:Z
Hx:0 <= x
F:forall n0 : Z, 1 < n0 < x -> rel_prime n0 p
Y:rel_prime x p
n:Z
HH1:1 < n
HH2:n < Z.succ x
rel_prime n p
p, m:Z
H1:1 < m
x:Z
Hx:0 <= x
F:forall n : Z, 1 < n < x -> rel_prime n p
N:~ rel_prime x p
{forall n : Z, 1 < n < Z.succ x -> rel_prime n p} +
{exists n : Z, 1 < n < Z.succ x /\ ~ rel_prime n p}
p, m:Z
H1:1 < m
x:Z
Hx:0 <= x
E:exists n : Z, 1 < n < x /\ ~ rel_prime n p
{forall n : Z, 1 < n < Z.succ x -> rel_prime n p} +
{exists n : Z, 1 < n < Z.succ x /\ ~ rel_prime n p}
  rewrite Z.lt_succ_r in HH2.p, m:Z
H1:1 < m
x:Z
Hx:0 <= x
F:forall n0 : Z, 1 < n0 < x -> rel_prime n0 p
Y:rel_prime x p
n:Z
HH1:1 < n
HH2:n <= x
rel_prime n p
p, m:Z
H1:1 < m
x:Z
Hx:0 <= x
F:forall n : Z, 1 < n < x -> rel_prime n p
N:~ rel_prime x p
{forall n : Z, 1 < n < Z.succ x -> rel_prime n p} +
{exists n : Z, 1 < n < Z.succ x /\ ~ rel_prime n p}
p, m:Z
H1:1 < m
x:Z
Hx:0 <= x
E:exists n : Z, 1 < n < x /\ ~ rel_prime n p
{forall n : Z, 1 < n < Z.succ x -> rel_prime n p} +
{exists n : Z, 1 < n < Z.succ x /\ ~ rel_prime n p}
  Z.le_elim HH2; subst; auto with zarith.p, m:Z
H1:1 < m
x:Z
Hx:0 <= x
F:forall n : Z, 1 < n < x -> rel_prime n p
N:~ rel_prime x p
{forall n : Z, 1 < n < Z.succ x -> rel_prime n p} +
{exists n : Z, 1 < n < Z.succ x /\ ~ rel_prime n p}
p, m:Z
H1:1 < m
x:Z
Hx:0 <= x
E:exists n : Z, 1 < n < x /\ ~ rel_prime n p
{forall n : Z, 1 < n < Z.succ x -> rel_prime n p} +
{exists n : Z, 1 < n < Z.succ x /\ ~ rel_prime n p}
  -p, m:Z
H1:1 < m
x:Z
Hx:0 <= x
F:forall n : Z, 1 < n < x -> rel_prime n p
N:~ rel_prime x p
{forall n : Z, 1 < n < Z.succ x -> rel_prime n p} +
{exists n : Z, 1 < n < Z.succ x /\ ~ rel_prime n p} case (Z_lt_dec 1 x); intros HH1.p, m:Z
H1:1 < m
x:Z
Hx:0 <= x
F:forall n : Z, 1 < n < x -> rel_prime n p
N:~ rel_prime x p
HH1:1 < x
{forall n : Z, 1 < n < Z.succ x -> rel_prime n p} +
{exists n : Z, 1 < n < Z.succ x /\ ~ rel_prime n p}
p, m:Z
H1:1 < m
x:Z
Hx:0 <= x
F:forall n : Z, 1 < n < x -> rel_prime n p
N:~ rel_prime x p
HH1:~ 1 < x
{forall n : Z, 1 < n < Z.succ x -> rel_prime n p} +
{exists n : Z, 1 < n < Z.succ x /\ ~ rel_prime n p}
    *p, m:Z
H1:1 < m
x:Z
Hx:0 <= x
F:forall n : Z, 1 < n < x -> rel_prime n p
N:~ rel_prime x p
HH1:1 < x
{forall n : Z, 1 < n < Z.succ x -> rel_prime n p} +
{exists n : Z, 1 < n < Z.succ x /\ ~ rel_prime n p} right; exists x; split; auto with zarith.
    *p, m:Z
H1:1 < m
x:Z
Hx:0 <= x
F:forall n : Z, 1 < n < x -> rel_prime n p
N:~ rel_prime x p
HH1:~ 1 < x
{forall n : Z, 1 < n < Z.succ x -> rel_prime n p} +
{exists n : Z, 1 < n < Z.succ x /\ ~ rel_prime n p} left; intros n [HHH1 HHH2]; contradict HHH1; auto with zarith.
  -p, m:Z
H1:1 < m
x:Z
Hx:0 <= x
E:exists n : Z, 1 < n < x /\ ~ rel_prime n p
{forall n : Z, 1 < n < Z.succ x -> rel_prime n p} +
{exists n : Z, 1 < n < Z.succ x /\ ~ rel_prime n p} right; destruct E as (n,((H0,H2),H3)); exists n; auto with zarith.
Defined.

Definition prime_dec: forall p, { prime p }+{ ~ prime p }.forall p : Z, {prime p} + {~ prime p}
Proof.forall p : Z, {prime p} + {~ prime p}
  intros p; case (Z_lt_dec 1 p); intros H1.p:Z
H1:1 < p
{prime p} + {~ prime p}
p:Z
H1:~ 1 < p
{prime p} + {~ prime p}
  +p:Z
H1:1 < p
{prime p} + {~ prime p} case (prime_dec_aux p p); intros H2.p:Z
H1:1 < p
H2:forall n : Z, 1 < n < p -> rel_prime n p
{prime p} + {~ prime p}
p:Z
H1:1 < p
H2:exists n : Z, 1 < n < p /\ ~ rel_prime n p
{prime p} + {~ prime p}
    *p:Z
H1:1 < p
H2:forall n : Z, 1 < n < p -> rel_prime n p
{prime p} + {~ prime p} left; apply prime_intro; auto.p:Z
H1:1 < p
H2:forall n : Z, 1 < n < p -> rel_prime n p
forall n : Z, 1 <= n < p -> rel_prime n p
      intros n (Hn1,Hn2).p:Z
H1:1 < p
H2:forall n0 : Z, 1 < n0 < p -> rel_prime n0 p
n:Z
Hn1:1 <= n
Hn2:n < p
rel_prime n p Z.le_elim Hn1; auto; subst n.p:Z
H1:1 < p
H2:forall n : Z, 1 < n < p -> rel_prime n p
Hn2:1 < p
rel_prime 1 p
      constructor; auto with zarith.
    *p:Z
H1:1 < p
H2:exists n : Z, 1 < n < p /\ ~ rel_prime n p
{prime p} + {~ prime p} right; intros H3; inversion_clear H3 as [Hp1 Hp2].p:Z
H1:1 < p
H2:exists n : Z, 1 < n < p /\ ~ rel_prime n p
Hp1:1 < p
Hp2:forall n : Z, 1 <= n < p -> rel_prime n p
False
      case H2; intros n [Hn1 Hn2]; case Hn2; auto with zarith.
  +p:Z
H1:~ 1 < p
{prime p} + {~ prime p} right; intros H3; inversion_clear H3 as [Hp1 Hp2]; case H1; auto.
Defined.

Theorem not_prime_divide:
 forall p, 1 < p -> ~ prime p -> exists n, 1 < n < p  /\ (n | p).forall p : Z,
1 < p ->
~ prime p -> exists n : Z, 1 < n < p /\ (n | p)
Proof.forall p : Z,
1 < p ->
~ prime p -> exists n : Z, 1 < n < p /\ (n | p)
  intros p Hp Hp1.p:Z
Hp:1 < p
Hp1:~ prime p
exists n : Z, 1 < n < p /\ (n | p)
  case (prime_dec_aux p p); intros H1.p:Z
Hp:1 < p
Hp1:~ prime p
H1:forall n : Z, 1 < n < p -> rel_prime n p
exists n : Z, 1 < n < p /\ (n | p)
p:Z
Hp:1 < p
Hp1:~ prime p
H1:exists n : Z, 1 < n < p /\ ~ rel_prime n p
exists n : Z, 1 < n < p /\ (n | p)
  -p:Z
Hp:1 < p
Hp1:~ prime p
H1:forall n : Z, 1 < n < p -> rel_prime n p
exists n : Z, 1 < n < p /\ (n | p) elim Hp1; constructor; auto.p:Z
Hp:1 < p
Hp1:~ prime p
H1:forall n : Z, 1 < n < p -> rel_prime n p
forall n : Z, 1 <= n < p -> rel_prime n p
    intros n (Hn1,Hn2).p:Z
Hp:1 < p
Hp1:~ prime p
H1:forall n0 : Z, 1 < n0 < p -> rel_prime n0 p
n:Z
Hn1:1 <= n
Hn2:n < p
rel_prime n p
    Z.le_elim Hn1; auto with zarith.p:Z
Hp:1 < p
Hp1:~ prime p
H1:forall n0 : Z, 1 < n0 < p -> rel_prime n0 p
n:Z
Hn1:1 = n
Hn2:n < p
rel_prime n p
    subst n; constructor; auto with zarith.
  -p:Z
Hp:1 < p
Hp1:~ prime p
H1:exists n : Z, 1 < n < p /\ ~ rel_prime n p
exists n : Z, 1 < n < p /\ (n | p) case H1; intros n (Hn1,Hn2).p:Z
Hp:1 < p
Hp1:~ prime p
H1:exists n0 : Z, 1 < n0 < p /\ ~ rel_prime n0 p
n:Z
Hn1:1 < n < p
Hn2:~ rel_prime n p
exists n0 : Z, 1 < n0 < p /\ (n0 | p)
    destruct (Z_0_1_more _ (Z.gcd_nonneg n p)) as [H|[H|H]].p:Z
Hp:1 < p
Hp1:~ prime p
H1:exists n0 : Z, 1 < n0 < p /\ ~ rel_prime n0 p
n:Z
Hn1:1 < n < p
Hn2:~ rel_prime n p
H:Z.gcd n p = 0
exists n0 : Z, 1 < n0 < p /\ (n0 | p)
p:Z
Hp:1 < p
Hp1:~ prime p
H1:exists n0 : Z, 1 < n0 < p /\ ~ rel_prime n0 p
n:Z
Hn1:1 < n < p
Hn2:~ rel_prime n p
H:Z.gcd n p = 1
exists n0 : Z, 1 < n0 < p /\ (n0 | p)
p:Z
Hp:1 < p
Hp1:~ prime p
H1:exists n0 : Z, 1 < n0 < p /\ ~ rel_prime n0 p
n:Z
Hn1:1 < n < p
Hn2:~ rel_prime n p
H:1 < Z.gcd n p
exists n0 : Z, 1 < n0 < p /\ (n0 | p)
    +p:Z
Hp:1 < p
Hp1:~ prime p
H1:exists n0 : Z, 1 < n0 < p /\ ~ rel_prime n0 p
n:Z
Hn1:1 < n < p
Hn2:~ rel_prime n p
H:Z.gcd n p = 0
exists n0 : Z, 1 < n0 < p /\ (n0 | p) exfalso.p:Z
Hp:1 < p
Hp1:~ prime p
H1:exists n0 : Z, 1 < n0 < p /\ ~ rel_prime n0 p
n:Z
Hn1:1 < n < p
Hn2:~ rel_prime n p
H:Z.gcd n p = 0
False apply Z.gcd_eq_0_l in H.p:Z
Hp:1 < p
Hp1:~ prime p
H1:exists n0 : Z, 1 < n0 < p /\ ~ rel_prime n0 p
n:Z
Hn1:1 < n < p
Hn2:~ rel_prime n p
H:n = 0
False omega.
    +p:Z
Hp:1 < p
Hp1:~ prime p
H1:exists n0 : Z, 1 < n0 < p /\ ~ rel_prime n0 p
n:Z
Hn1:1 < n < p
Hn2:~ rel_prime n p
H:Z.gcd n p = 1
exists n0 : Z, 1 < n0 < p /\ (n0 | p) elim Hn2.p:Z
Hp:1 < p
Hp1:~ prime p
H1:exists n0 : Z, 1 < n0 < p /\ ~ rel_prime n0 p
n:Z
Hn1:1 < n < p
Hn2:~ rel_prime n p
H:Z.gcd n p = 1
rel_prime n p red.p:Z
Hp:1 < p
Hp1:~ prime p
H1:exists n0 : Z, 1 < n0 < p /\ ~ rel_prime n0 p
n:Z
Hn1:1 < n < p
Hn2:~ rel_prime n p
H:Z.gcd n p = 1
Zis_gcd n p 1 rewrite <- H.p:Z
Hp:1 < p
Hp1:~ prime p
H1:exists n0 : Z, 1 < n0 < p /\ ~ rel_prime n0 p
n:Z
Hn1:1 < n < p
Hn2:~ rel_prime n p
H:Z.gcd n p = 1
Zis_gcd n p (Z.gcd n p) apply Zgcd_is_gcd.
    +p:Z
Hp:1 < p
Hp1:~ prime p
H1:exists n0 : Z, 1 < n0 < p /\ ~ rel_prime n0 p
n:Z
Hn1:1 < n < p
Hn2:~ rel_prime n p
H:1 < Z.gcd n p
exists n0 : Z, 1 < n0 < p /\ (n0 | p) exists (Z.gcd n p); split; [ split; auto | apply Z.gcd_divide_r ].p:Z
Hp:1 < p
Hp1:~ prime p
H1:exists n0 : Z, 1 < n0 < p /\ ~ rel_prime n0 p
n:Z
Hn1:1 < n < p
Hn2:~ rel_prime n p
H:1 < Z.gcd n p
Z.gcd n p < p
      apply Z.le_lt_trans with n; auto with zarith.p:Z
Hp:1 < p
Hp1:~ prime p
H1:exists n0 : Z, 1 < n0 < p /\ ~ rel_prime n0 p
n:Z
Hn1:1 < n < p
Hn2:~ rel_prime n p
H:1 < Z.gcd n p
Z.gcd n p <= n
      apply Z.divide_pos_le; auto with zarith.p:Z
Hp:1 < p
Hp1:~ prime p
H1:exists n0 : Z, 1 < n0 < p /\ ~ rel_prime n0 p
n:Z
Hn1:1 < n < p
Hn2:~ rel_prime n p
H:1 < Z.gcd n p
(Z.gcd n p | n)
      apply Z.gcd_divide_l.
Qed.