NZGcd.v

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)         *)
(************************************************************************)

Greatest Common Divisor

Require Import NZAxioms NZMulOrder.

Interface of a gcd function, then its specification on naturals

Module Type Gcd (Import A : Typ).
 Parameter Inline gcd : t -> t -> t.
End Gcd.

Module Type NZGcdSpec (A : NZOrdAxiomsSig')(B : Gcd A).
 Import A B.
 Definition divide n m := exists p, m == p*n.
 Local Notation "( n | m )" := (divide n m) (at level 0).
 Axiom gcd_divide_l : forall n m, (gcd n m | n).
 Axiom gcd_divide_r : forall n m, (gcd n m | m).
 Axiom gcd_greatest : forall n m p, (p | n) -> (p | m) -> (p | gcd n m).
 Axiom gcd_nonneg : forall n m, 0 <= gcd n m.
End NZGcdSpec.

Module Type DivideNotation (A:NZOrdAxiomsSig')(B:Gcd A)(C:NZGcdSpec A B).
 Import A B C.
 Notation "( n | m )" := (divide n m) (at level 0).
End DivideNotation.

Module Type NZGcd (A : NZOrdAxiomsSig) := Gcd A <+ NZGcdSpec A.
Module Type NZGcd' (A : NZOrdAxiomsSig) :=
 Gcd A <+ NZGcdSpec A <+ DivideNotation A.

Derived properties of gcd

Module NZGcdProp
 (Import A : NZOrdAxiomsSig')
 (Import B : NZGcd' A)
 (Import C : NZMulOrderProp A).

Results concerning divisibility

Instance divide_wd : Proper (eq==>eq==>iff) divide.Proper (eq ==> eq ==> iff) divide
Proof.Proper (eq ==> eq ==> iff) divide
 unfold divide.Proper (eq ==> eq ==> iff)
  (fun n m : t => exists p : t, m == p * n) intros x x' Hx y y' Hy.x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
(exists p : t, y == p * x) <->
(exists p : t, y' == p * x')
 setoid_rewrite Hx.x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
(exists p : t, y == p * x') <->
(exists p : t, y' == p * x') setoid_rewrite Hy.x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
(exists p : t, y' == p * x') <->
(exists p : t, y' == p * x') easy.
Qed.

Lemma divide_1_l : forall n, (1 | n).forall n : t, (1 | n)
Proof.forall n : t, (1 | n)
 intros n.n:t
(1 | n) exists n.n:t
n == n * 1 now nzsimpl.
Qed.

Lemma divide_0_r : forall n, (n | 0).forall n : t, (n | 0)
Proof.forall n : t, (n | 0)
 intros n.n:t
(n | 0) exists 0.n:t
0 == 0 * n now nzsimpl.
Qed.

Lemma divide_0_l : forall n, (0 | n) -> n==0.forall n : t, (0 | n) -> n == 0
Proof.forall n : t, (0 | n) -> n == 0
 intros n (m,Hm).n, m:t
Hm:n == m * 0
n == 0 revert Hm.n, m:t
n == m * 0 -> n == 0 now nzsimpl.
Qed.

Lemma eq_mul_1_nonneg : forall n m,
 0<=n -> n*m == 1 -> n==1 /\ m==1.forall n m : t,
0 <= n -> n * m == 1 -> n == 1 /\ m == 1
Proof.forall n m : t,
0 <= n -> n * m == 1 -> n == 1 /\ m == 1
 intros n m Hn H.n, m:t
Hn:0 <= n
H:n * m == 1
n == 1 /\ m == 1
 le_elim Hn.n, m:t
Hn:0 < n
H:n * m == 1
n == 1 /\ m == 1
n, m:t
Hn:0 == n
H:n * m == 1
n == 1 /\ m == 1
 -n, m:t
Hn:0 < n
H:n * m == 1
n == 1 /\ m == 1 destruct (lt_ge_cases m 0) as [Hm|Hm].n, m:t
Hn:0 < n
H:n * m == 1
Hm:m < 0
n == 1 /\ m == 1
n, m:t
Hn:0 < n
H:n * m == 1
Hm:0 <= m
n == 1 /\ m == 1
   +n, m:t
Hn:0 < n
H:n * m == 1
Hm:m < 0
n == 1 /\ m == 1 generalize (mul_pos_neg n m Hn Hm).n, m:t
Hn:0 < n
H:n * m == 1
Hm:m < 0
n * m < 0 -> n == 1 /\ m == 1 order'.
   +n, m:t
Hn:0 < n
H:n * m == 1
Hm:0 <= m
n == 1 /\ m == 1 le_elim Hm.n, m:t
Hn:0 < n
H:n * m == 1
Hm:0 < m
n == 1 /\ m == 1
n, m:t
Hn:0 < n
H:n * m == 1
Hm:0 == m
n == 1 /\ m == 1
     *n, m:t
Hn:0 < n
H:n * m == 1
Hm:0 < m
n == 1 /\ m == 1 apply le_succ_l in Hn.n, m:t
Hn:S 0 <= n
H:n * m == 1
Hm:0 < m
n == 1 /\ m == 1 rewrite <- one_succ in Hn.n, m:t
Hn:1 <= n
H:n * m == 1
Hm:0 < m
n == 1 /\ m == 1
       le_elim Hn.n, m:t
Hn:1 < n
H:n * m == 1
Hm:0 < m
n == 1 /\ m == 1
n, m:t
Hn:1 == n
H:n * m == 1
Hm:0 < m
n == 1 /\ m == 1
       --n, m:t
Hn:1 < n
H:n * m == 1
Hm:0 < m
n == 1 /\ m == 1 generalize (lt_1_mul_pos n m Hn Hm).n, m:t
Hn:1 < n
H:n * m == 1
Hm:0 < m
1 < n * m -> n == 1 /\ m == 1 order.
       --n, m:t
Hn:1 == n
H:n * m == 1
Hm:0 < m
n == 1 /\ m == 1 rewrite <- Hn, mul_1_l in H.n, m:t
Hn:1 == n
H:m == 1
Hm:0 < m
n == 1 /\ m == 1 now split.
     *n, m:t
Hn:0 < n
H:n * m == 1
Hm:0 == m
n == 1 /\ m == 1 rewrite <- Hm, mul_0_r in H.n, m:t
Hn:0 < n
H:0 == 1
Hm:0 == m
n == 1 /\ m == 1 order'.
 -n, m:t
Hn:0 == n
H:n * m == 1
n == 1 /\ m == 1 rewrite <- Hn, mul_0_l in H.n, m:t
Hn:0 == n
H:0 == 1
n == 1 /\ m == 1 order'.
Qed.

Lemma eq_mul_1_nonneg' : forall n m,
 0<=m -> n*m == 1 -> n==1 /\ m==1.forall n m : t,
0 <= m -> n * m == 1 -> n == 1 /\ m == 1
Proof.forall n m : t,
0 <= m -> n * m == 1 -> n == 1 /\ m == 1
 intros n m Hm H.n, m:t
Hm:0 <= m
H:n * m == 1
n == 1 /\ m == 1 rewrite mul_comm in H.n, m:t
Hm:0 <= m
H:m * n == 1
n == 1 /\ m == 1
 now apply and_comm, eq_mul_1_nonneg.
Qed.

Lemma divide_1_r_nonneg : forall n, 0<=n -> (n | 1) -> n==1.forall n : t, 0 <= n -> (n | 1) -> n == 1
Proof.forall n : t, 0 <= n -> (n | 1) -> n == 1
 intros n Hn (m,Hm).n:t
Hn:0 <= n
m:t
Hm:1 == m * n
n == 1 symmetry in Hm.n:t
Hn:0 <= n
m:t
Hm:m * n == 1
n == 1
 now apply (eq_mul_1_nonneg' m n).
Qed.

Lemma divide_refl : forall n, (n | n).forall n : t, (n | n)
Proof.forall n : t, (n | n)
 intros n.n:t
(n | n) exists 1.n:t
n == 1 * n now nzsimpl.
Qed.

Lemma divide_trans : forall n m p, (n | m) -> (m | p) -> (n | p).forall n m p : t, (n | m) -> (m | p) -> (n | p)
Proof.forall n m p : t, (n | m) -> (m | p) -> (n | p)
 intros n m p (q,Hq) (r,Hr).n, m, p, q:t
Hq:m == q * n
r:t
Hr:p == r * m
(n | p) exists (r*q).n, m, p, q:t
Hq:m == q * n
r:t
Hr:p == r * m
p == r * q * n
 now rewrite Hr, Hq, mul_assoc.
Qed.

Instance divide_reflexive : Reflexive divide | 5 := divide_refl.
Instance divide_transitive : Transitive divide | 5 := divide_trans.

Due to sign, no general antisymmetry result

Lemma divide_antisym_nonneg : forall n m,
 0<=n -> 0<=m -> (n | m) -> (m | n) -> n == m.forall n m : t,
0 <= n -> 0 <= m -> (n | m) -> (m | n) -> n == m
Proof.forall n m : t,
0 <= n -> 0 <= m -> (n | m) -> (m | n) -> n == m
 intros n m Hn Hm (q,Hq) (r,Hr).n, m:t
Hn:0 <= n
Hm:0 <= m
q:t
Hq:m == q * n
r:t
Hr:n == r * m
n == m
 le_elim Hn.n, m:t
Hn:0 < n
Hm:0 <= m
q:t
Hq:m == q * n
r:t
Hr:n == r * m
n == m
n, m:t
Hn:0 == n
Hm:0 <= m
q:t
Hq:m == q * n
r:t
Hr:n == r * m
n == m
 -n, m:t
Hn:0 < n
Hm:0 <= m
q:t
Hq:m == q * n
r:t
Hr:n == r * m
n == m destruct (lt_ge_cases q 0) as [Hq'|Hq'].n, m:t
Hn:0 < n
Hm:0 <= m
q:t
Hq:m == q * n
r:t
Hr:n == r * m
Hq':q < 0
n == m
n, m:t
Hn:0 < n
Hm:0 <= m
q:t
Hq:m == q * n
r:t
Hr:n == r * m
Hq':0 <= q
n == m
   +n, m:t
Hn:0 < n
Hm:0 <= m
q:t
Hq:m == q * n
r:t
Hr:n == r * m
Hq':q < 0
n == m generalize (mul_neg_pos q n Hq' Hn).n, m:t
Hn:0 < n
Hm:0 <= m
q:t
Hq:m == q * n
r:t
Hr:n == r * m
Hq':q < 0
q * n < 0 -> n == m order.
   +n, m:t
Hn:0 < n
Hm:0 <= m
q:t
Hq:m == q * n
r:t
Hr:n == r * m
Hq':0 <= q
n == m rewrite Hq, mul_assoc in Hr.n, m:t
Hn:0 < n
Hm:0 <= m
q:t
Hq:m == q * n
r:t
Hr:n == r * q * n
Hq':0 <= q
n == m symmetry in Hr.n, m:t
Hn:0 < n
Hm:0 <= m
q:t
Hq:m == q * n
r:t
Hr:r * q * n == n
Hq':0 <= q
n == m
     apply mul_id_l in Hr; [|order].n, m:t
Hn:0 < n
Hm:0 <= m
q:t
Hq:m == q * n
r:t
Hr:r * q == 1
Hq':0 <= q
n == m
     destruct (eq_mul_1_nonneg' r q) as [_ H]; trivial.n, m:t
Hn:0 < n
Hm:0 <= m
q:t
Hq:m == q * n
r:t
Hr:r * q == 1
Hq':0 <= q
H:q == 1
n == m
     now rewrite H, mul_1_l in Hq.
 -n, m:t
Hn:0 == n
Hm:0 <= m
q:t
Hq:m == q * n
r:t
Hr:n == r * m
n == m rewrite <- Hn, mul_0_r in Hq.n, m:t
Hn:0 == n
Hm:0 <= m
q:t
Hq:m == 0
r:t
Hr:n == r * m
n == m now rewrite <- Hn.
Qed.

Lemma mul_divide_mono_l : forall n m p, (n | m) -> (p * n | p * m).forall n m p : t, (n | m) -> (p * n | p * m)
Proof.forall n m p : t, (n | m) -> (p * n | p * m)
 intros n m p (q,Hq).n, m, p, q:t
Hq:m == q * n
(p * n | p * m) exists q.n, m, p, q:t
Hq:m == q * n
p * m == q * (p * n) now rewrite mul_shuffle3, Hq.
Qed.

Lemma mul_divide_mono_r : forall n m p, (n | m) -> (n * p | m * p).forall n m p : t, (n | m) -> (n * p | m * p)
Proof.forall n m p : t, (n | m) -> (n * p | m * p)
 intros n m p (q,Hq).n, m, p, q:t
Hq:m == q * n
(n * p | m * p) exists q.n, m, p, q:t
Hq:m == q * n
m * p == q * (n * p) now rewrite mul_assoc, Hq.
Qed.

Lemma mul_divide_cancel_l : forall n m p, p ~= 0 ->
 ((p * n | p * m) <-> (n | m)).forall n m p : t,
p ~= 0 -> (p * n | p * m) <-> (n | m)
Proof.forall n m p : t,
p ~= 0 -> (p * n | p * m) <-> (n | m)
 intros n m p Hp.n, m, p:t
Hp:p ~= 0
(p * n | p * m) <-> (n | m) split.n, m, p:t
Hp:p ~= 0
(p * n | p * m) -> (n | m)
n, m, p:t
Hp:p ~= 0
(n | m) -> (p * n | p * m)
 -n, m, p:t
Hp:p ~= 0
(p * n | p * m) -> (n | m) intros (q,Hq).n, m, p:t
Hp:p ~= 0
q:t
Hq:p * m == q * (p * n)
(n | m) exists q.n, m, p:t
Hp:p ~= 0
q:t
Hq:p * m == q * (p * n)
m == q * n now rewrite mul_shuffle3, mul_cancel_l in Hq.
 -n, m, p:t
Hp:p ~= 0
(n | m) -> (p * n | p * m) apply mul_divide_mono_l.
Qed.

Lemma mul_divide_cancel_r : forall n m p, p ~= 0 ->
 ((n * p | m * p) <-> (n | m)).forall n m p : t,
p ~= 0 -> (n * p | m * p) <-> (n | m)
Proof.forall n m p : t,
p ~= 0 -> (n * p | m * p) <-> (n | m)
 intros.n, m, p:t
H:p ~= 0
(n * p | m * p) <-> (n | m) rewrite 2 (mul_comm _ p).n, m, p:t
H:p ~= 0
(p * n | p * m) <-> (n | m) now apply mul_divide_cancel_l.
Qed.

Lemma divide_add_r : forall n m p, (n | m) -> (n | p) -> (n | m + p).forall n m p : t, (n | m) -> (n | p) -> (n | m + p)
Proof.forall n m p : t, (n | m) -> (n | p) -> (n | m + p)
 intros n m p (q,Hq) (r,Hr).n, m, p, q:t
Hq:m == q * n
r:t
Hr:p == r * n
(n | m + p) exists (q+r).n, m, p, q:t
Hq:m == q * n
r:t
Hr:p == r * n
m + p == (q + r) * n
 now rewrite mul_add_distr_r, Hq, Hr.
Qed.

Lemma divide_mul_l : forall n m p, (n | m) -> (n | m * p).forall n m p : t, (n | m) -> (n | m * p)
Proof.forall n m p : t, (n | m) -> (n | m * p)
 intros n m p (q,Hq).n, m, p, q:t
Hq:m == q * n
(n | m * p) exists (q*p).n, m, p, q:t
Hq:m == q * n
m * p == q * p * n now rewrite mul_shuffle0, Hq.
Qed.

Lemma divide_mul_r : forall n m p, (n | p) -> (n | m * p).forall n m p : t, (n | p) -> (n | m * p)
Proof.forall n m p : t, (n | p) -> (n | m * p)
 intros n m p.n, m, p:t
(n | p) -> (n | m * p) rewrite mul_comm.n, m, p:t
(n | p) -> (n | p * m) apply divide_mul_l.
Qed.

Lemma divide_factor_l : forall n m, (n | n * m).forall n m : t, (n | n * m)
Proof.forall n m : t, (n | n * m)
 intros.n, m:t
(n | n * m) apply divide_mul_l, divide_refl.
Qed.

Lemma divide_factor_r : forall n m, (n | m * n).forall n m : t, (n | m * n)
Proof.forall n m : t, (n | m * n)
 intros.n, m:t
(n | m * n) apply divide_mul_r, divide_refl.
Qed.

Lemma divide_pos_le : forall n m, 0 < m -> (n | m) -> n <= m.forall n m : t, 0 < m -> (n | m) -> n <= m
Proof.forall n m : t, 0 < m -> (n | m) -> n <= m
 intros n m Hm (q,Hq).n, m:t
Hm:0 < m
q:t
Hq:m == q * n
n <= m
 destruct (le_gt_cases n 0) as [Hn|Hn].n, m:t
Hm:0 < m
q:t
Hq:m == q * n
Hn:n <= 0
n <= m
n, m:t
Hm:0 < m
q:t
Hq:m == q * n
Hn:0 < n
n <= m -n, m:t
Hm:0 < m
q:t
Hq:m == q * n
Hn:n <= 0
n <= m order.
 -n, m:t
Hm:0 < m
q:t
Hq:m == q * n
Hn:0 < n
n <= m rewrite Hq.n, m:t
Hm:0 < m
q:t
Hq:m == q * n
Hn:0 < n
n <= q * n
   destruct (lt_ge_cases q 0) as [Hq'|Hq'].n, m:t
Hm:0 < m
q:t
Hq:m == q * n
Hn:0 < n
Hq':q < 0
n <= q * n
n, m:t
Hm:0 < m
q:t
Hq:m == q * n
Hn:0 < n
Hq':0 <= q
n <= q * n
   +n, m:t
Hm:0 < m
q:t
Hq:m == q * n
Hn:0 < n
Hq':q < 0
n <= q * n generalize (mul_neg_pos q n Hq' Hn).n, m:t
Hm:0 < m
q:t
Hq:m == q * n
Hn:0 < n
Hq':q < 0
q * n < 0 -> n <= q * n order.
   +n, m:t
Hm:0 < m
q:t
Hq:m == q * n
Hn:0 < n
Hq':0 <= q
n <= q * n le_elim Hq'.n, m:t
Hm:0 < m
q:t
Hq:m == q * n
Hn:0 < n
Hq':0 < q
n <= q * n
n, m:t
Hm:0 < m
q:t
Hq:m == q * n
Hn:0 < n
Hq':0 == q
n <= q * n
     *n, m:t
Hm:0 < m
q:t
Hq:m == q * n
Hn:0 < n
Hq':0 < q
n <= q * n rewrite <- (mul_1_l n) at 1.n, m:t
Hm:0 < m
q:t
Hq:m == q * n
Hn:0 < n
Hq':0 < q
1 * n <= q * n apply mul_le_mono_pos_r; trivial.n, m:t
Hm:0 < m
q:t
Hq:m == q * n
Hn:0 < n
Hq':0 < q
1 <= q
       now rewrite one_succ, le_succ_l.
     *n, m:t
Hm:0 < m
q:t
Hq:m == q * n
Hn:0 < n
Hq':0 == q
n <= q * n rewrite <- Hq', mul_0_l in Hq.n, m:t
Hm:0 < m
q:t
Hq:m == 0
Hn:0 < n
Hq':0 == q
n <= q * n order.
Qed.

Basic properties of gcd

Lemma gcd_unique : forall n m p,
 0<=p -> (p|n) -> (p|m) ->
 (forall q, (q|n) -> (q|m) -> (q|p)) ->
 gcd n m == p.forall n m p : t,
0 <= p ->
(p | n) ->
(p | m) ->
(forall q : t, (q | n) -> (q | m) -> (q | p)) ->
gcd n m == p
Proof.forall n m p : t,
0 <= p ->
(p | n) ->
(p | m) ->
(forall q : t, (q | n) -> (q | m) -> (q | p)) ->
gcd n m == p
 intros n m p Hp Hn Hm H.n, m, p:t
Hp:0 <= p
Hn:(p | n)
Hm:(p | m)
H:forall q : t, (q | n) -> (q | m) -> (q | p)
gcd n m == p
 apply divide_antisym_nonneg; trivial.n, m, p:t
Hp:0 <= p
Hn:(p | n)
Hm:(p | m)
H:forall q : t, (q | n) -> (q | m) -> (q | p)
0 <= gcd n m
n, m, p:t
Hp:0 <= p
Hn:(p | n)
Hm:(p | m)
H:forall q : t, (q | n) -> (q | m) -> (q | p)
(gcd n m | p)
n, m, p:t
Hp:0 <= p
Hn:(p | n)
Hm:(p | m)
H:forall q : t, (q | n) -> (q | m) -> (q | p)
(p | gcd n m) -n, m, p:t
Hp:0 <= p
Hn:(p | n)
Hm:(p | m)
H:forall q : t, (q | n) -> (q | m) -> (q | p)
0 <= gcd n m apply gcd_nonneg.
 -n, m, p:t
Hp:0 <= p
Hn:(p | n)
Hm:(p | m)
H:forall q : t, (q | n) -> (q | m) -> (q | p)
(gcd n m | p) apply H.n, m, p:t
Hp:0 <= p
Hn:(p | n)
Hm:(p | m)
H:forall q : t, (q | n) -> (q | m) -> (q | p)
(gcd n m | n)
n, m, p:t
Hp:0 <= p
Hn:(p | n)
Hm:(p | m)
H:forall q : t, (q | n) -> (q | m) -> (q | p)
(gcd n m | m) +n, m, p:t
Hp:0 <= p
Hn:(p | n)
Hm:(p | m)
H:forall q : t, (q | n) -> (q | m) -> (q | p)
(gcd n m | n) apply gcd_divide_l. +n, m, p:t
Hp:0 <= p
Hn:(p | n)
Hm:(p | m)
H:forall q : t, (q | n) -> (q | m) -> (q | p)
(gcd n m | m) apply gcd_divide_r.
 -n, m, p:t
Hp:0 <= p
Hn:(p | n)
Hm:(p | m)
H:forall q : t, (q | n) -> (q | m) -> (q | p)
(p | gcd n m) now apply gcd_greatest.
Qed.

Instance gcd_wd : Proper (eq==>eq==>eq) gcd.Proper (eq ==> eq ==> eq) gcd
Proof.Proper (eq ==> eq ==> eq) gcd
 intros x x' Hx y y' Hy.x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
gcd x y == gcd x' y'
 apply gcd_unique.x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
0 <= gcd x' y'
x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
(gcd x' y' | x)
x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
(gcd x' y' | y)
x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
forall q : t, (q | x) -> (q | y) -> (q | gcd x' y')
 -x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
0 <= gcd x' y' apply gcd_nonneg.
 -x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
(gcd x' y' | x) rewrite Hx.x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
(gcd x' y' | x') apply gcd_divide_l.
 -x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
(gcd x' y' | y) rewrite Hy.x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
(gcd x' y' | y') apply gcd_divide_r.
 -x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
forall q : t, (q | x) -> (q | y) -> (q | gcd x' y') intro.x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
q:t
(q | x) -> (q | y) -> (q | gcd x' y') rewrite Hx, Hy.x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
q:t
(q | x') -> (q | y') -> (q | gcd x' y') apply gcd_greatest.
Qed.

Lemma gcd_divide_iff : forall n m p,
  (p | gcd n m) <-> (p | n) /\ (p | m).forall n m p : t, (p | gcd n m) <-> (p | n) /\ (p | m)
Proof.forall n m p : t, (p | gcd n m) <-> (p | n) /\ (p | m)
  intros.n, m, p:t
(p | gcd n m) <-> (p | n) /\ (p | m) split.n, m, p:t
(p | gcd n m) -> (p | n) /\ (p | m)
n, m, p:t
(p | n) /\ (p | m) -> (p | gcd n m) -n, m, p:t
(p | gcd n m) -> (p | n) /\ (p | m) split.n, m, p:t
H:(p | gcd n m)
(p | n)
n, m, p:t
H:(p | gcd n m)
(p | m)
                   +n, m, p:t
H:(p | gcd n m)
(p | n) transitivity (gcd n m); trivial using gcd_divide_l.
                   +n, m, p:t
H:(p | gcd n m)
(p | m) transitivity (gcd n m); trivial using gcd_divide_r.
  -n, m, p:t
(p | n) /\ (p | m) -> (p | gcd n m) intros (H,H').n, m, p:t
H:(p | n)
H':(p | m)
(p | gcd n m) now apply gcd_greatest.
Qed.

Lemma gcd_unique_alt : forall n m p, 0<=p ->
 (forall q, (q|p) <-> (q|n) /\ (q|m)) ->
 gcd n m == p.forall n m p : t,
0 <= p ->
(forall q : t, (q | p) <-> (q | n) /\ (q | m)) ->
gcd n m == p
Proof.forall n m p : t,
0 <= p ->
(forall q : t, (q | p) <-> (q | n) /\ (q | m)) ->
gcd n m == p
 intros n m p Hp H.n, m, p:t
Hp:0 <= p
H:forall q : t, (q | p) <-> (q | n) /\ (q | m)
gcd n m == p
 apply gcd_unique; trivial.n, m, p:t
Hp:0 <= p
H:forall q : t, (q | p) <-> (q | n) /\ (q | m)
(p | n)
n, m, p:t
Hp:0 <= p
H:forall q : t, (q | p) <-> (q | n) /\ (q | m)
(p | m)
n, m, p:t
Hp:0 <= p
H:forall q : t, (q | p) <-> (q | n) /\ (q | m)
forall q : t, (q | n) -> (q | m) -> (q | p)
 -n, m, p:t
Hp:0 <= p
H:forall q : t, (q | p) <-> (q | n) /\ (q | m)
(p | n) apply H.n, m, p:t
Hp:0 <= p
H:forall q : t, (q | p) <-> (q | n) /\ (q | m)
(p | p) apply divide_refl.
 -n, m, p:t
Hp:0 <= p
H:forall q : t, (q | p) <-> (q | n) /\ (q | m)
(p | m) apply H.n, m, p:t
Hp:0 <= p
H:forall q : t, (q | p) <-> (q | n) /\ (q | m)
(p | p) apply divide_refl.
 -n, m, p:t
Hp:0 <= p
H:forall q : t, (q | p) <-> (q | n) /\ (q | m)
forall q : t, (q | n) -> (q | m) -> (q | p) intros.n, m, p:t
Hp:0 <= p
H:forall q0 : t, (q0 | p) <-> (q0 | n) /\ (q0 | m)
q:t
H0:(q | n)
H1:(q | m)
(q | p) apply H.n, m, p:t
Hp:0 <= p
H:forall q0 : t, (q0 | p) <-> (q0 | n) /\ (q0 | m)
q:t
H0:(q | n)
H1:(q | m)
(q | n) /\ (q | m) now split.
Qed.

Lemma gcd_comm : forall n m, gcd n m == gcd m n.forall n m : t, gcd n m == gcd m n
Proof.forall n m : t, gcd n m == gcd m n
 intros.n, m:t
gcd n m == gcd m n apply gcd_unique_alt; try apply gcd_nonneg.n, m:t
forall q : t, (q | gcd m n) <-> (q | n) /\ (q | m)
 intros.n, m, q:t
(q | gcd m n) <-> (q | n) /\ (q | m) rewrite and_comm.n, m, q:t
(q | gcd m n) <-> (q | m) /\ (q | n) apply gcd_divide_iff.
Qed.

Lemma gcd_assoc : forall n m p, gcd n (gcd m p) == gcd (gcd n m) p.forall n m p : t, gcd n (gcd m p) == gcd (gcd n m) p
Proof.forall n m p : t, gcd n (gcd m p) == gcd (gcd n m) p
 intros.n, m, p:t
gcd n (gcd m p) == gcd (gcd n m) p apply gcd_unique_alt; try apply gcd_nonneg.n, m, p:t
forall q : t,
(q | gcd (gcd n m) p) <-> (q | n) /\ (q | gcd m p)
 intros.n, m, p, q:t
(q | gcd (gcd n m) p) <-> (q | n) /\ (q | gcd m p) now rewrite !gcd_divide_iff, and_assoc.
Qed.

Lemma gcd_0_l_nonneg : forall n, 0<=n -> gcd 0 n == n.forall n : t, 0 <= n -> gcd 0 n == n
Proof.forall n : t, 0 <= n -> gcd 0 n == n
 intros.n:t
H:0 <= n
gcd 0 n == n apply gcd_unique; trivial.n:t
H:0 <= n
(n | 0)
n:t
H:0 <= n
(n | n)
 -n:t
H:0 <= n
(n | 0) apply divide_0_r.
 -n:t
H:0 <= n
(n | n) apply divide_refl.
Qed.

Lemma gcd_0_r_nonneg : forall n, 0<=n -> gcd n 0 == n.forall n : t, 0 <= n -> gcd n 0 == n
Proof.forall n : t, 0 <= n -> gcd n 0 == n
 intros.n:t
H:0 <= n
gcd n 0 == n now rewrite gcd_comm, gcd_0_l_nonneg.
Qed.

Lemma gcd_1_l : forall n, gcd 1 n == 1.forall n : t, gcd 1 n == 1
Proof.forall n : t, gcd 1 n == 1
 intros.n:t
gcd 1 n == 1 apply gcd_unique; trivial using divide_1_l, le_0_1.
Qed.

Lemma gcd_1_r : forall n, gcd n 1 == 1.forall n : t, gcd n 1 == 1
Proof.forall n : t, gcd n 1 == 1
 intros.n:t
gcd n 1 == 1 now rewrite gcd_comm, gcd_1_l.
Qed.

Lemma gcd_diag_nonneg : forall n, 0<=n -> gcd n n == n.forall n : t, 0 <= n -> gcd n n == n
Proof.forall n : t, 0 <= n -> gcd n n == n
 intros.n:t
H:0 <= n
gcd n n == n apply gcd_unique; trivial using divide_refl.
Qed.

Lemma gcd_eq_0_l : forall n m, gcd n m == 0 -> n == 0.forall n m : t, gcd n m == 0 -> n == 0
Proof.forall n m : t, gcd n m == 0 -> n == 0
 intros.n, m:t
H:gcd n m == 0
n == 0
 generalize (gcd_divide_l n m).n, m:t
H:gcd n m == 0
(gcd n m | n) -> n == 0 rewrite H.n, m:t
H:gcd n m == 0
(0 | n) -> n == 0 apply divide_0_l.
Qed.

Lemma gcd_eq_0_r : forall n m, gcd n m == 0 -> m == 0.forall n m : t, gcd n m == 0 -> m == 0
Proof.forall n m : t, gcd n m == 0 -> m == 0
 intros.n, m:t
H:gcd n m == 0
m == 0 apply gcd_eq_0_l with n.n, m:t
H:gcd n m == 0
gcd m n == 0 now rewrite gcd_comm.
Qed.

Lemma gcd_eq_0 : forall n m, gcd n m == 0 <-> n == 0 /\ m == 0.forall n m : t, gcd n m == 0 <-> n == 0 /\ m == 0
Proof.forall n m : t, gcd n m == 0 <-> n == 0 /\ m == 0
  intros.n, m:t
gcd n m == 0 <-> n == 0 /\ m == 0 split.n, m:t
gcd n m == 0 -> n == 0 /\ m == 0
n, m:t
n == 0 /\ m == 0 -> gcd n m == 0
  -n, m:t
gcd n m == 0 -> n == 0 /\ m == 0 split.n, m:t
H:gcd n m == 0
n == 0
n, m:t
H:gcd n m == 0
m == 0
    +n, m:t
H:gcd n m == 0
n == 0 now apply gcd_eq_0_l with m.
    +n, m:t
H:gcd n m == 0
m == 0 now apply gcd_eq_0_r with n.
  -n, m:t
n == 0 /\ m == 0 -> gcd n m == 0 intros (EQ,EQ').n, m:t
EQ:n == 0
EQ':m == 0
gcd n m == 0 rewrite EQ, EQ'.n, m:t
EQ:n == 0
EQ':m == 0
gcd 0 0 == 0 now apply gcd_0_r_nonneg.
Qed.

Lemma gcd_mul_diag_l : forall n m, 0<=n -> gcd n (n*m) == n.forall n m : t, 0 <= n -> gcd n (n * m) == n
Proof.forall n m : t, 0 <= n -> gcd n (n * m) == n
 intros n m Hn.n, m:t
Hn:0 <= n
gcd n (n * m) == n apply gcd_unique_alt; trivial.n, m:t
Hn:0 <= n
forall q : t, (q | n) <-> (q | n) /\ (q | n * m)
 intros q.n, m:t
Hn:0 <= n
q:t
(q | n) <-> (q | n) /\ (q | n * m) split.n, m:t
Hn:0 <= n
q:t
(q | n) -> (q | n) /\ (q | n * m)
n, m:t
Hn:0 <= n
q:t
(q | n) /\ (q | n * m) -> (q | n) -n, m:t
Hn:0 <= n
q:t
(q | n) -> (q | n) /\ (q | n * m) split; trivial.n, m:t
Hn:0 <= n
q:t
H:(q | n)
(q | n * m) now apply divide_mul_l.
 -n, m:t
Hn:0 <= n
q:t
(q | n) /\ (q | n * m) -> (q | n) now destruct 1.
Qed.

Lemma divide_gcd_iff : forall n m, 0<=n -> ((n|m) <-> gcd n m == n).forall n m : t, 0 <= n -> (n | m) <-> gcd n m == n
Proof.forall n m : t, 0 <= n -> (n | m) <-> gcd n m == n
  intros n m Hn.n, m:t
Hn:0 <= n
(n | m) <-> gcd n m == n split.n, m:t
Hn:0 <= n
(n | m) -> gcd n m == n
n, m:t
Hn:0 <= n
gcd n m == n -> (n | m)
  -n, m:t
Hn:0 <= n
(n | m) -> gcd n m == n intros (q,Hq).n, m:t
Hn:0 <= n
q:t
Hq:m == q * n
gcd n m == n rewrite Hq.n, m:t
Hn:0 <= n
q:t
Hq:m == q * n
gcd n (q * n) == n
    rewrite mul_comm.n, m:t
Hn:0 <= n
q:t
Hq:m == q * n
gcd n (n * q) == n now apply gcd_mul_diag_l.
  -n, m:t
Hn:0 <= n
gcd n m == n -> (n | m) intros EQ.n, m:t
Hn:0 <= n
EQ:gcd n m == n
(n | m) rewrite <- EQ.n, m:t
Hn:0 <= n
EQ:gcd n m == n
(gcd n m | m) apply gcd_divide_r.
Qed.

End NZGcdProp.