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

Properties of the greatest common divisor

Require Import ZAxioms ZMulOrder ZSgnAbs NZGcd.

Module Type ZGcdProp
 (Import A : ZAxiomsSig')
 (Import B : ZMulOrderProp A)
 (Import C : ZSgnAbsProp A B).

 Include NZGcdProp A A B.

Results concerning divisibility

Lemma divide_opp_l : forall n m, (-n | m) <-> (n | m).forall n m : t, (- n | m) <-> (n | m)
Proof.forall n m : t, (- n | m) <-> (n | m)
 intros n m.n, m:t
(- n | m) <-> (n | m) split; intros (p,Hp); exists (-p); rewrite Hp.n, m, p:t
Hp:m == p * - n
p * - n == - p * n
n, m, p:t
Hp:m == p * n
p * n == - p * - n
  now rewrite mul_opp_l, mul_opp_r.n, m, p:t
Hp:m == p * n
p * n == - p * - n
  now rewrite mul_opp_opp.
Qed.

Lemma divide_opp_r : forall n m, (n | -m) <-> (n | m).forall n m : t, (n | - m) <-> (n | m)
Proof.forall n m : t, (n | - m) <-> (n | m)
 intros n m.n, m:t
(n | - m) <-> (n | m) split; intros (p,Hp); exists (-p).n, m, p:t
Hp:- m == p * n
m == - p * n
n, m, p:t
Hp:m == p * n
- m == - p * n
  now rewrite mul_opp_l, <- Hp, opp_involutive.n, m, p:t
Hp:m == p * n
- m == - p * n
  now rewrite Hp, mul_opp_l.
Qed.

Lemma divide_abs_l : forall n m, (abs n | m) <-> (n | m).forall n m : t, (abs n | m) <-> (n | m)
Proof.forall n m : t, (abs n | m) <-> (n | m)
 intros n m.n, m:t
(abs n | m) <-> (n | m) destruct (abs_eq_or_opp n) as [H|H]; rewrite H.n, m:t
H:abs n == n
(n | m) <-> (n | m)
n, m:t
H:abs n == - n
(- n | m) <-> (n | m)
 easy.n, m:t
H:abs n == - n
(- n | m) <-> (n | m) apply divide_opp_l.
Qed.

Lemma divide_abs_r : forall n m, (n | abs m) <-> (n | m).forall n m : t, (n | abs m) <-> (n | m)
Proof.forall n m : t, (n | abs m) <-> (n | m)
 intros n m.n, m:t
(n | abs m) <-> (n | m) destruct (abs_eq_or_opp m) as [H|H]; rewrite H.n, m:t
H:abs m == m
(n | m) <-> (n | m)
n, m:t
H:abs m == - m
(n | - m) <-> (n | m)
 easy.n, m:t
H:abs m == - m
(n | - m) <-> (n | m) apply divide_opp_r.
Qed.

Lemma divide_1_r_abs : forall n, (n | 1) -> abs n == 1.forall n : t, (n | 1) -> abs n == 1
Proof.forall n : t, (n | 1) -> abs n == 1
 intros n Hn.n:t
Hn:(n | 1)
abs n == 1 apply divide_1_r_nonneg.n:t
Hn:(n | 1)
0 <= abs n
n:t
Hn:(n | 1)
(abs n | 1) apply abs_nonneg.n:t
Hn:(n | 1)
(abs n | 1)
 now apply divide_abs_l.
Qed.

Lemma divide_1_r : forall n, (n | 1) -> n==1 \/ n==-1.forall n : t, (n | 1) -> n == 1 \/ n == -1
Proof.forall n : t, (n | 1) -> n == 1 \/ n == -1
 intros n (m,H).n, m:t
H:1 == m * n
n == 1 \/ n == -1 rewrite mul_comm in H.n, m:t
H:1 == n * m
n == 1 \/ n == -1 now apply eq_mul_1 with m.
Qed.

Lemma divide_antisym_abs : forall n m,
 (n | m) -> (m | n) -> abs n == abs m.forall n m : t, (n | m) -> (m | n) -> abs n == abs m
Proof.forall n m : t, (n | m) -> (m | n) -> abs n == abs m
 intros.n, m:t
H:(n | m)
H0:(m | n)
abs n == abs m apply divide_antisym_nonneg; try apply abs_nonneg.n, m:t
H:(n | m)
H0:(m | n)
(abs n | abs m)
n, m:t
H:(n | m)
H0:(m | n)
(abs m | abs n)
 now apply divide_abs_l, divide_abs_r.n, m:t
H:(n | m)
H0:(m | n)
(abs m | abs n)
 now apply divide_abs_l, divide_abs_r.
Qed.

Lemma divide_antisym : forall n m,
 (n | m) -> (m | n) -> n == m \/ n == -m.forall n m : t,
(n | m) -> (m | n) -> n == m \/ n == - m
Proof.forall n m : t,
(n | m) -> (m | n) -> n == m \/ n == - m
 intros.n, m:t
H:(n | m)
H0:(m | n)
n == m \/ n == - m now apply abs_eq_cases, divide_antisym_abs.
Qed.

Lemma divide_sub_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 H H'.n, m, p:t
H:(n | m)
H':(n | p)
(n | m - p) rewrite <- add_opp_r.n, m, p:t
H:(n | m)
H':(n | p)
(n | m + - p)
 apply divide_add_r; trivial.n, m, p:t
H:(n | m)
H':(n | p)
(n | - p) now apply divide_opp_r.
Qed.

Lemma divide_add_cancel_r : forall n m p, (n | m) -> (n | m + p) -> (n | p).forall n m p : t, (n | m) -> (n | m + p) -> (n | p)
Proof.forall n m p : t, (n | m) -> (n | m + p) -> (n | p)
 intros n m p H H'.n, m, p:t
H:(n | m)
H':(n | m + p)
(n | p) rewrite <- (add_simpl_l m p).n, m, p:t
H:(n | m)
H':(n | m + p)
(n | m + p - m) now apply divide_sub_r.
Qed.

Properties of gcd

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

Lemma gcd_opp_r : forall n m, gcd n (-m) == gcd n m.forall n m : t, gcd n (- m) == gcd n m
Proof.forall n m : t, gcd n (- m) == gcd n m
 intros.n, m:t
gcd n (- m) == gcd n m now rewrite gcd_comm, gcd_opp_l, gcd_comm.
Qed.

Lemma gcd_abs_l : forall n m, gcd (abs n) m == gcd n m.forall n m : t, gcd (abs n) m == gcd n m
Proof.forall n m : t, gcd (abs n) m == gcd n m
 intros.n, m:t
gcd (abs n) m == gcd n m destruct (abs_eq_or_opp n) as [H|H]; rewrite H.n, m:t
H:abs n == n
gcd n m == gcd n m
n, m:t
H:abs n == - n
gcd (- n) m == gcd n m
 easy.n, m:t
H:abs n == - n
gcd (- n) m == gcd n m apply gcd_opp_l.
Qed.

Lemma gcd_abs_r : forall n m, gcd n (abs m) == gcd n m.forall n m : t, gcd n (abs m) == gcd n m
Proof.forall n m : t, gcd n (abs m) == gcd n m
 intros.n, m:t
gcd n (abs m) == gcd n m now rewrite gcd_comm, gcd_abs_l, gcd_comm.
Qed.

Lemma gcd_0_l : forall n, gcd 0 n == abs n.forall n : t, gcd 0 n == abs n
Proof.forall n : t, gcd 0 n == abs n
 intros.n:t
gcd 0 n == abs n rewrite <- gcd_abs_r.n:t
gcd 0 (abs n) == abs n apply gcd_0_l_nonneg, abs_nonneg.
Qed.

Lemma gcd_0_r : forall n, gcd n 0 == abs n.forall n : t, gcd n 0 == abs n
Proof.forall n : t, gcd n 0 == abs n
 intros.n:t
gcd n 0 == abs n now rewrite gcd_comm, gcd_0_l.
Qed.

Lemma gcd_diag : forall n, gcd n n == abs n.forall n : t, gcd n n == abs n
Proof.forall n : t, gcd n n == abs n
 intros.n:t
gcd n n == abs n rewrite <- gcd_abs_l, <- gcd_abs_r.n:t
gcd (abs n) (abs n) == abs n
 apply gcd_diag_nonneg, abs_nonneg.
Qed.

Lemma gcd_add_mult_diag_r : forall n m p, gcd n (m+p*n) == gcd n m.forall n m p : t, gcd n (m + p * n) == gcd n m
Proof.forall n m p : t, gcd n (m + p * n) == gcd n m
 intros.n, m, p:t
gcd n (m + p * n) == gcd n m apply gcd_unique_alt; try apply gcd_nonneg.n, m, p:t
forall q : t,
(q | gcd n m) <-> (q | n) /\ (q | m + p * n)
 intros.n, m, p, q:t
(q | gcd n m) <-> (q | n) /\ (q | m + p * n) rewrite gcd_divide_iff.n, m, p, q:t
(q | n) /\ (q | m) <-> (q | n) /\ (q | m + p * n) split; intros (U,V); split; trivial.n, m, p, q:t
U:(q | n)
V:(q | m)
(q | m + p * n)
n, m, p, q:t
U:(q | n)
V:(q | m + p * n)
(q | m)
 apply divide_add_r; trivial.n, m, p, q:t
U:(q | n)
V:(q | m)
(q | p * n)
n, m, p, q:t
U:(q | n)
V:(q | m + p * n)
(q | m) now apply divide_mul_r.n, m, p, q:t
U:(q | n)
V:(q | m + p * n)
(q | m)
 apply divide_add_cancel_r with (p*n); trivial.n, m, p, q:t
U:(q | n)
V:(q | m + p * n)
(q | p * n)
n, m, p, q:t
U:(q | n)
V:(q | m + p * n)
(q | p * n + m)
 now apply divide_mul_r.n, m, p, q:t
U:(q | n)
V:(q | m + p * n)
(q | p * n + m) now rewrite add_comm.
Qed.

Lemma gcd_add_diag_r : forall n m, gcd n (m+n) == gcd n m.forall n m : t, gcd n (m + n) == gcd n m
Proof.forall n m : t, gcd n (m + n) == gcd n m
 intros n m.n, m:t
gcd n (m + n) == gcd n m rewrite <- (mul_1_l n) at 2.n, m:t
gcd n (m + 1 * n) == gcd n m apply gcd_add_mult_diag_r.
Qed.

Lemma gcd_sub_diag_r : forall n m, gcd n (m-n) == gcd n m.forall n m : t, gcd n (m - n) == gcd n m
Proof.forall n m : t, gcd n (m - n) == gcd n m
 intros n m.n, m:t
gcd n (m - n) == gcd n m rewrite <- (mul_1_l n) at 2.n, m:t
gcd n (m - 1 * n) == gcd n m
 rewrite <- add_opp_r, <- mul_opp_l.n, m:t
gcd n (m + -1 * n) == gcd n m apply gcd_add_mult_diag_r.
Qed.

Definition Bezout n m p := exists a b, a*n + b*m == p.

Instance Bezout_wd : Proper (eq==>eq==>eq==>iff) Bezout.Proper (eq ==> eq ==> eq ==> iff) Bezout
Proof.Proper (eq ==> eq ==> eq ==> iff) Bezout
 unfold Bezout.Proper (eq ==> eq ==> eq ==> iff)
  (fun n m p : t => exists a b : t, a * n + b * m == p) intros x x' Hx y y' Hy z z' Hz.x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
z, z':t
Hz:z == z'
(exists a b : t, a * x + b * y == z) <->
(exists a b : t, a * x' + b * y' == z')
 setoid_rewrite Hx.x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
z, z':t
Hz:z == z'
(exists a b : t, a * x' + b * y == z) <->
(exists a b : t, a * x' + b * y' == z') setoid_rewrite Hy.x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
z, z':t
Hz:z == z'
(exists a b : t, a * x' + b * y' == z) <->
(exists a b : t, a * x' + b * y' == z') now setoid_rewrite Hz.
Qed.

Lemma bezout_1_gcd : forall n m, Bezout n m 1 -> gcd n m == 1.forall n m : t, Bezout n m 1 -> gcd n m == 1
Proof.forall n m : t, Bezout n m 1 -> gcd n m == 1
 intros n m (q & r & H).n, m, q, r:t
H:q * n + r * m == 1
gcd n m == 1
 apply gcd_unique; trivial using divide_1_l, le_0_1.n, m, q, r:t
H:q * n + r * m == 1
forall q0 : t, (q0 | n) -> (q0 | m) -> (q0 | 1)
 intros p Hn Hm.n, m, q, r:t
H:q * n + r * m == 1
p:t
Hn:(p | n)
Hm:(p | m)
(p | 1)
 rewrite <- H.n, m, q, r:t
H:q * n + r * m == 1
p:t
Hn:(p | n)
Hm:(p | m)
(p | q * n + r * m) apply divide_add_r; now apply divide_mul_r.
Qed.

Lemma gcd_bezout : forall n m p, gcd n m == p -> Bezout n m p.forall n m p : t, gcd n m == p -> Bezout n m p
Proof.forall n m p : t, gcd n m == p -> Bezout n m p
 (* First, a version restricted to natural numbers *)
 assert (aux : forall n, 0<=n -> forall m, 0<=m -> Bezout n m (gcd n m)).forall n : t,
0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p
  intros n Hn; pattern n.n:t
Hn:0 <= n
(fun t0 : t =>
 forall m : t, 0 <= m -> Bezout t0 m (gcd t0 m)) n
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p
  apply strong_right_induction with (z:=0); trivial.n:t
Hn:0 <= n
Proper (eq ==> iff)
  (fun t0 : t =>
   forall m : t, 0 <= m -> Bezout t0 m (gcd t0 m))
n:t
Hn:0 <= n
forall n0 : t,
0 <= n0 ->
(forall m : t,
 0 <= m ->
 m < n0 ->
 forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)) ->
forall m : t, 0 <= m -> Bezout n0 m (gcd n0 m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p
  unfold Bezout.n:t
Hn:0 <= n
Proper (eq ==> iff)
  (fun t0 : t =>
   forall m : t,
   0 <= m ->
   exists a b : t, a * t0 + b * m == gcd t0 m)
n:t
Hn:0 <= n
forall n0 : t,
0 <= n0 ->
(forall m : t,
 0 <= m ->
 m < n0 ->
 forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)) ->
forall m : t, 0 <= m -> Bezout n0 m (gcd n0 m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p solve_proper.n:t
Hn:0 <= n
forall n0 : t,
0 <= n0 ->
(forall m : t,
 0 <= m ->
 m < n0 ->
 forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)) ->
forall m : t, 0 <= m -> Bezout n0 m (gcd n0 m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p
  clear n Hn.forall n : t,
0 <= n ->
(forall m : t,
 0 <= m ->
 m < n ->
 forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)) ->
forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p intros n Hn IHn.n:t
Hn:0 <= n
IHn:forall m : t,
0 <= m -> m < n -> forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)
forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p
  apply le_lteq in Hn; destruct Hn as [Hn|Hn].n:t
Hn:0 < n
IHn:forall m : t,
0 <= m -> m < n -> forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)
forall m : t, 0 <= m -> Bezout n m (gcd n m)
n:t
Hn:0 == n
IHn:forall m : t,
0 <= m -> m < n -> forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)
forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p
  intros m Hm; pattern m.n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
(fun t0 : t => Bezout n t0 (gcd n t0)) m
n:t
Hn:0 == n
IHn:forall m : t,
0 <= m -> m < n -> forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)
forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p
  apply strong_right_induction with (z:=0); trivial.n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
Proper (eq ==> iff)
  (fun t0 : t => Bezout n t0 (gcd n t0))
n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
forall n0 : t,
0 <= n0 ->
(forall m0 : t,
 0 <= m0 -> m0 < n0 -> Bezout n m0 (gcd n m0)) ->
Bezout n n0 (gcd n n0)
n:t
Hn:0 == n
IHn:forall m : t,
0 <= m -> m < n -> forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)
forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p
  unfold Bezout.n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
Proper (eq ==> iff)
  (fun t0 : t =>
   exists a b : t, a * n + b * t0 == gcd n t0)
n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
forall n0 : t,
0 <= n0 ->
(forall m0 : t,
 0 <= m0 -> m0 < n0 -> Bezout n m0 (gcd n m0)) ->
Bezout n n0 (gcd n n0)
n:t
Hn:0 == n
IHn:forall m : t,
0 <= m -> m < n -> forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)
forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p solve_proper.n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
forall n0 : t,
0 <= n0 ->
(forall m0 : t,
 0 <= m0 -> m0 < n0 -> Bezout n m0 (gcd n m0)) ->
Bezout n n0 (gcd n n0)
n:t
Hn:0 == n
IHn:forall m : t,
0 <= m -> m < n -> forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)
forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p
  clear m Hm.n:t
Hn:0 < n
IHn:forall m : t,
0 <= m -> m < n -> forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)
forall n0 : t,
0 <= n0 ->
(forall m : t,
 0 <= m -> m < n0 -> Bezout n m (gcd n m)) ->
Bezout n n0 (gcd n n0)
n:t
Hn:0 == n
IHn:forall m : t,
0 <= m -> m < n -> forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)
forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p intros m Hm IHm.n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
Bezout n m (gcd n m)
n:t
Hn:0 == n
IHn:forall m : t,
0 <= m -> m < n -> forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)
forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p
  destruct (lt_trichotomy n m) as [LT|[EQ|LT]].n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:n < m
Bezout n m (gcd n m)
n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
EQ:n == m
Bezout n m (gcd n m)
n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:m < n
Bezout n m (gcd n m)
n:t
Hn:0 == n
IHn:forall m : t,
0 <= m -> m < n -> forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)
forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p
  (* n < m *)
  destruct (IHm (m-n)) as (a & b & EQ).n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:n < m
0 <= m - n
n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:n < m
m - n < m
n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:n < m
a, b:t
EQ:a * n + b * (m - n) == gcd n (m - n)
Bezout n m (gcd n m)
n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
EQ:n == m
Bezout n m (gcd n m)
n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:m < n
Bezout n m (gcd n m)
n:t
Hn:0 == n
IHn:forall m : t,
0 <= m -> m < n -> forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)
forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p
  apply sub_nonneg; order.n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:n < m
m - n < m
n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:n < m
a, b:t
EQ:a * n + b * (m - n) == gcd n (m - n)
Bezout n m (gcd n m)
n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
EQ:n == m
Bezout n m (gcd n m)
n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:m < n
Bezout n m (gcd n m)
n:t
Hn:0 == n
IHn:forall m : t,
0 <= m -> m < n -> forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)
forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p
  now apply lt_sub_pos.n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:n < m
a, b:t
EQ:a * n + b * (m - n) == gcd n (m - n)
Bezout n m (gcd n m)
n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
EQ:n == m
Bezout n m (gcd n m)
n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:m < n
Bezout n m (gcd n m)
n:t
Hn:0 == n
IHn:forall m : t,
0 <= m -> m < n -> forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)
forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p
  exists (a-b).n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:n < m
a, b:t
EQ:a * n + b * (m - n) == gcd n (m - n)
exists b0 : t, (a - b) * n + b0 * m == gcd n m
n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
EQ:n == m
Bezout n m (gcd n m)
n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:m < n
Bezout n m (gcd n m)
n:t
Hn:0 == n
IHn:forall m : t,
0 <= m -> m < n -> forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)
forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p exists b.n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:n < m
a, b:t
EQ:a * n + b * (m - n) == gcd n (m - n)
(a - b) * n + b * m == gcd n m
n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
EQ:n == m
Bezout n m (gcd n m)
n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:m < n
Bezout n m (gcd n m)
n:t
Hn:0 == n
IHn:forall m : t,
0 <= m -> m < n -> forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)
forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p
  rewrite gcd_sub_diag_r in EQ.n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:n < m
a, b:t
EQ:a * n + b * (m - n) == gcd n m
(a - b) * n + b * m == gcd n m
n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
EQ:n == m
Bezout n m (gcd n m)
n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:m < n
Bezout n m (gcd n m)
n:t
Hn:0 == n
IHn:forall m : t,
0 <= m -> m < n -> forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)
forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p rewrite <- EQ.n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:n < m
a, b:t
EQ:a * n + b * (m - n) == gcd n m
(a - b) * n + b * m == a * n + b * (m - n)
n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
EQ:n == m
Bezout n m (gcd n m)
n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:m < n
Bezout n m (gcd n m)
n:t
Hn:0 == n
IHn:forall m : t,
0 <= m -> m < n -> forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)
forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p
  rewrite mul_sub_distr_r, mul_sub_distr_l.n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:n < m
a, b:t
EQ:a * n + b * (m - n) == gcd n m
a * n - b * n + b * m == a * n + (b * m - b * n)
n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
EQ:n == m
Bezout n m (gcd n m)
n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:m < n
Bezout n m (gcd n m)
n:t
Hn:0 == n
IHn:forall m : t,
0 <= m -> m < n -> forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)
forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p
  now rewrite add_sub_assoc, add_sub_swap.n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
EQ:n == m
Bezout n m (gcd n m)
n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:m < n
Bezout n m (gcd n m)
n:t
Hn:0 == n
IHn:forall m : t,
0 <= m -> m < n -> forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)
forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p
  (* n = m *)
  rewrite EQ.n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
EQ:n == m
Bezout m m (gcd m m)
n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:m < n
Bezout n m (gcd n m)
n:t
Hn:0 == n
IHn:forall m : t,
0 <= m -> m < n -> forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)
forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p rewrite gcd_diag_nonneg; trivial.n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
EQ:n == m
Bezout m m m
n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:m < n
Bezout n m (gcd n m)
n:t
Hn:0 == n
IHn:forall m : t,
0 <= m -> m < n -> forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)
forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p
  exists 1.n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
EQ:n == m
exists b : t, 1 * m + b * m == m
n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:m < n
Bezout n m (gcd n m)
n:t
Hn:0 == n
IHn:forall m : t,
0 <= m -> m < n -> forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)
forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p exists 0.n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
EQ:n == m
1 * m + 0 * m == m
n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:m < n
Bezout n m (gcd n m)
n:t
Hn:0 == n
IHn:forall m : t,
0 <= m -> m < n -> forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)
forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p now nzsimpl.n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:m < n
Bezout n m (gcd n m)
n:t
Hn:0 == n
IHn:forall m : t,
0 <= m -> m < n -> forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)
forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p
  (* m < n *)
  destruct (IHn m Hm LT n) as (a & b & EQ).n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:m < n
0 <= n
n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:m < n
a, b:t
EQ:a * m + b * n == gcd m n
Bezout n m (gcd n m)
n:t
Hn:0 == n
IHn:forall m : t,
0 <= m -> m < n -> forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)
forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p order.n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:m < n
a, b:t
EQ:a * m + b * n == gcd m n
Bezout n m (gcd n m)
n:t
Hn:0 == n
IHn:forall m : t,
0 <= m -> m < n -> forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)
forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p
  exists b.n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:m < n
a, b:t
EQ:a * m + b * n == gcd m n
exists b0 : t, b * n + b0 * m == gcd n m
n:t
Hn:0 == n
IHn:forall m : t,
0 <= m -> m < n -> forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)
forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p exists a.n:t
Hn:0 < n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
IHm:forall m0 : t, 0 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0)
LT:m < n
a, b:t
EQ:a * m + b * n == gcd m n
b * n + a * m == gcd n m
n:t
Hn:0 == n
IHn:forall m : t,
0 <= m -> m < n -> forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)
forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p now rewrite gcd_comm, <- EQ, add_comm.n:t
Hn:0 == n
IHn:forall m : t,
0 <= m -> m < n -> forall m0 : t, 0 <= m0 -> Bezout m m0 (gcd m m0)
forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p
  (* n = 0 *)
  intros m Hm.n:t
Hn:0 == n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p rewrite <- Hn, gcd_0_l_nonneg; trivial.n:t
Hn:0 == n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
Bezout 0 m m
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p
  exists 0.n:t
Hn:0 == n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
exists b : t, 0 * 0 + b * m == m
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p exists 1.n:t
Hn:0 == n
IHn:forall m0 : t,
0 <= m0 -> m0 < n -> forall m1 : t, 0 <= m1 -> Bezout m0 m1 (gcd m0 m1)
m:t
Hm:0 <= m
0 * 0 + 1 * m == m
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p now nzsimpl.aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p
 (* Then we relax the positivity condition on n *)
 assert (aux' : forall n m, 0<=m -> Bezout n m (gcd n m)).aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m : t, 0 <= m -> Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux':forall n m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p
  intros n m Hm.aux:forall n0 : t, 0 <= n0 -> forall m0 : t, 0 <= m0 -> Bezout n0 m0 (gcd n0 m0)
n, m:t
Hm:0 <= m
Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux':forall n m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p
  destruct (le_ge_cases 0 n).aux:forall n0 : t, 0 <= n0 -> forall m0 : t, 0 <= m0 -> Bezout n0 m0 (gcd n0 m0)
n, m:t
Hm:0 <= m
H:0 <= n
Bezout n m (gcd n m)
aux:forall n0 : t, 0 <= n0 -> forall m0 : t, 0 <= m0 -> Bezout n0 m0 (gcd n0 m0)
n, m:t
Hm:0 <= m
H:n <= 0
Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux':forall n m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p now apply aux.aux:forall n0 : t, 0 <= n0 -> forall m0 : t, 0 <= m0 -> Bezout n0 m0 (gcd n0 m0)
n, m:t
Hm:0 <= m
H:n <= 0
Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux':forall n m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p
  assert (Hn' : 0 <= -n) by now apply opp_nonneg_nonpos.aux:forall n0 : t, 0 <= n0 -> forall m0 : t, 0 <= m0 -> Bezout n0 m0 (gcd n0 m0)
n, m:t
Hm:0 <= m
H:n <= 0
Hn':0 <= - n
Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux':forall n m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p
  destruct (aux (-n) Hn' m Hm) as (a & b & EQ).aux:forall n0 : t, 0 <= n0 -> forall m0 : t, 0 <= m0 -> Bezout n0 m0 (gcd n0 m0)
n, m:t
Hm:0 <= m
H:n <= 0
Hn':0 <= - n
a, b:t
EQ:a * - n + b * m == gcd (- n) m
Bezout n m (gcd n m)
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux':forall n m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p
  exists (-a).aux:forall n0 : t, 0 <= n0 -> forall m0 : t, 0 <= m0 -> Bezout n0 m0 (gcd n0 m0)
n, m:t
Hm:0 <= m
H:n <= 0
Hn':0 <= - n
a, b:t
EQ:a * - n + b * m == gcd (- n) m
exists b0 : t, - a * n + b0 * m == gcd n m
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux':forall n m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p exists b.aux:forall n0 : t, 0 <= n0 -> forall m0 : t, 0 <= m0 -> Bezout n0 m0 (gcd n0 m0)
n, m:t
Hm:0 <= m
H:n <= 0
Hn':0 <= - n
a, b:t
EQ:a * - n + b * m == gcd (- n) m
- a * n + b * m == gcd n m
aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux':forall n m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p now rewrite <- gcd_opp_l, <- EQ, mul_opp_r, mul_opp_l.aux:forall n : t, 0 <= n -> forall m : t, 0 <= m -> Bezout n m (gcd n m)
aux':forall n m : t, 0 <= m -> Bezout n m (gcd n m)
forall n m p : t, gcd n m == p -> Bezout n m p
 (* And finally we do the same for m *)
 intros n m p Hp.aux:forall n0 : t, 0 <= n0 -> forall m0 : t, 0 <= m0 -> Bezout n0 m0 (gcd n0 m0)
aux':forall n0 m0 : t,
0 <= m0 -> Bezout n0 m0 (gcd n0 m0)
n, m, p:t
Hp:gcd n m == p
Bezout n m p rewrite <- Hp; clear Hp.aux:forall n0 : t, 0 <= n0 -> forall m0 : t, 0 <= m0 -> Bezout n0 m0 (gcd n0 m0)
aux':forall n0 m0 : t,
0 <= m0 -> Bezout n0 m0 (gcd n0 m0)
n, m, p:t
Bezout n m (gcd n m)
 destruct (le_ge_cases 0 m).aux:forall n0 : t, 0 <= n0 -> forall m0 : t, 0 <= m0 -> Bezout n0 m0 (gcd n0 m0)
aux':forall n0 m0 : t,
0 <= m0 -> Bezout n0 m0 (gcd n0 m0)
n, m, p:t
H:0 <= m
Bezout n m (gcd n m)
aux:forall n0 : t,
0 <= n0 ->
forall m0 : t,
0 <= m0 -> Bezout n0 m0 (gcd n0 m0)
aux':forall n0 m0 : t,
0 <= m0 -> Bezout n0 m0 (gcd n0 m0)
n, m, p:t
H:m <= 0
Bezout n m (gcd n m) now apply aux'.aux:forall n0 : t, 0 <= n0 -> forall m0 : t, 0 <= m0 -> Bezout n0 m0 (gcd n0 m0)
aux':forall n0 m0 : t,
0 <= m0 -> Bezout n0 m0 (gcd n0 m0)
n, m, p:t
H:m <= 0
Bezout n m (gcd n m)
 assert (Hm' : 0 <= -m) by now apply opp_nonneg_nonpos.aux:forall n0 : t, 0 <= n0 -> forall m0 : t, 0 <= m0 -> Bezout n0 m0 (gcd n0 m0)
aux':forall n0 m0 : t,
0 <= m0 -> Bezout n0 m0 (gcd n0 m0)
n, m, p:t
H:m <= 0
Hm':0 <= - m
Bezout n m (gcd n m)
 destruct (aux' n (-m) Hm') as (a & b & EQ).aux:forall n0 : t, 0 <= n0 -> forall m0 : t, 0 <= m0 -> Bezout n0 m0 (gcd n0 m0)
aux':forall n0 m0 : t,
0 <= m0 -> Bezout n0 m0 (gcd n0 m0)
n, m, p:t
H:m <= 0
Hm':0 <= - m
a, b:t
EQ:a * n + b * - m == gcd n (- m)
Bezout n m (gcd n m)
 exists a.aux:forall n0 : t, 0 <= n0 -> forall m0 : t, 0 <= m0 -> Bezout n0 m0 (gcd n0 m0)
aux':forall n0 m0 : t,
0 <= m0 -> Bezout n0 m0 (gcd n0 m0)
n, m, p:t
H:m <= 0
Hm':0 <= - m
a, b:t
EQ:a * n + b * - m == gcd n (- m)
exists b0 : t, a * n + b0 * m == gcd n m exists (-b).aux:forall n0 : t, 0 <= n0 -> forall m0 : t, 0 <= m0 -> Bezout n0 m0 (gcd n0 m0)
aux':forall n0 m0 : t,
0 <= m0 -> Bezout n0 m0 (gcd n0 m0)
n, m, p:t
H:m <= 0
Hm':0 <= - m
a, b:t
EQ:a * n + b * - m == gcd n (- m)
a * n + - b * m == gcd n m now rewrite <- gcd_opp_r, <- EQ, mul_opp_r, mul_opp_l.
Qed.

Lemma gcd_mul_mono_l :
  forall n m p, gcd (p * n) (p * m) == abs p * gcd n m.forall n m p : t,
gcd (p * n) (p * m) == abs p * gcd n m
Proof.forall n m p : t,
gcd (p * n) (p * m) == abs p * gcd n m
 intros n m p.n, m, p:t
gcd (p * n) (p * m) == abs p * gcd n m
 apply gcd_unique.n, m, p:t
0 <= abs p * gcd n m
n, m, p:t
(abs p * gcd n m | p * n)
n, m, p:t
(abs p * gcd n m | p * m)
n, m, p:t
forall q : t,
(q | p * n) -> (q | p * m) -> (q | abs p * gcd n m)
 apply mul_nonneg_nonneg; trivial using gcd_nonneg, abs_nonneg.n, m, p:t
(abs p * gcd n m | p * n)
n, m, p:t
(abs p * gcd n m | p * m)
n, m, p:t
forall q : t,
(q | p * n) -> (q | p * m) -> (q | abs p * gcd n m)
 destruct (gcd_divide_l n m) as (q,Hq).n, m, p, q:t
Hq:n == q * gcd n m
(abs p * gcd n m | p * n)
n, m, p:t
(abs p * gcd n m | p * m)
n, m, p:t
forall q : t,
(q | p * n) -> (q | p * m) -> (q | abs p * gcd n m)
 rewrite Hq at 2.n, m, p, q:t
Hq:n == q * gcd n m
(abs p * gcd n m | p * (q * gcd n m))
n, m, p:t
(abs p * gcd n m | p * m)
n, m, p:t
forall q : t,
(q | p * n) -> (q | p * m) -> (q | abs p * gcd n m) rewrite mul_assoc.n, m, p, q:t
Hq:n == q * gcd n m
(abs p * gcd n m | p * q * gcd n m)
n, m, p:t
(abs p * gcd n m | p * m)
n, m, p:t
forall q : t,
(q | p * n) -> (q | p * m) -> (q | abs p * gcd n m) apply mul_divide_mono_r.n, m, p, q:t
Hq:n == q * gcd n m
(abs p | p * q)
n, m, p:t
(abs p * gcd n m | p * m)
n, m, p:t
forall q : t,
(q | p * n) -> (q | p * m) -> (q | abs p * gcd n m)
 rewrite <- (abs_sgn p) at 2.n, m, p, q:t
Hq:n == q * gcd n m
(abs p | abs p * sgn p * q)
n, m, p:t
(abs p * gcd n m | p * m)
n, m, p:t
forall q : t,
(q | p * n) -> (q | p * m) -> (q | abs p * gcd n m) rewrite <- mul_assoc.n, m, p, q:t
Hq:n == q * gcd n m
(abs p | abs p * (sgn p * q))
n, m, p:t
(abs p * gcd n m | p * m)
n, m, p:t
forall q : t,
(q | p * n) -> (q | p * m) -> (q | abs p * gcd n m) apply divide_factor_l.n, m, p:t
(abs p * gcd n m | p * m)
n, m, p:t
forall q : t,
(q | p * n) -> (q | p * m) -> (q | abs p * gcd n m)
 destruct (gcd_divide_r n m) as (q,Hq).n, m, p, q:t
Hq:m == q * gcd n m
(abs p * gcd n m | p * m)
n, m, p:t
forall q : t,
(q | p * n) -> (q | p * m) -> (q | abs p * gcd n m)
 rewrite Hq at 2.n, m, p, q:t
Hq:m == q * gcd n m
(abs p * gcd n m | p * (q * gcd n m))
n, m, p:t
forall q : t,
(q | p * n) -> (q | p * m) -> (q | abs p * gcd n m) rewrite mul_assoc.n, m, p, q:t
Hq:m == q * gcd n m
(abs p * gcd n m | p * q * gcd n m)
n, m, p:t
forall q : t,
(q | p * n) -> (q | p * m) -> (q | abs p * gcd n m) apply mul_divide_mono_r.n, m, p, q:t
Hq:m == q * gcd n m
(abs p | p * q)
n, m, p:t
forall q : t,
(q | p * n) -> (q | p * m) -> (q | abs p * gcd n m)
 rewrite <- (abs_sgn p) at 2.n, m, p, q:t
Hq:m == q * gcd n m
(abs p | abs p * sgn p * q)
n, m, p:t
forall q : t,
(q | p * n) -> (q | p * m) -> (q | abs p * gcd n m) rewrite <- mul_assoc.n, m, p, q:t
Hq:m == q * gcd n m
(abs p | abs p * (sgn p * q))
n, m, p:t
forall q : t,
(q | p * n) -> (q | p * m) -> (q | abs p * gcd n m) apply divide_factor_l.n, m, p:t
forall q : t,
(q | p * n) -> (q | p * m) -> (q | abs p * gcd n m)
 intros q H H'.n, m, p, q:t
H:(q | p * n)
H':(q | p * m)
(q | abs p * gcd n m)
 destruct (gcd_bezout n m (gcd n m) (eq_refl _)) as (a & b & EQ).n, m, p, q:t
H:(q | p * n)
H':(q | p * m)
a, b:t
EQ:a * n + b * m == gcd n m
(q | abs p * gcd n m)
 rewrite <- EQ, <- sgn_abs, mul_add_distr_l.n, m, p, q:t
H:(q | p * n)
H':(q | p * m)
a, b:t
EQ:a * n + b * m == gcd n m
(q | p * sgn p * (a * n) + p * sgn p * (b * m)) apply divide_add_r.n, m, p, q:t
H:(q | p * n)
H':(q | p * m)
a, b:t
EQ:a * n + b * m == gcd n m
(q | p * sgn p * (a * n))
n, m, p, q:t
H:(q | p * n)
H':(q | p * m)
a, b:t
EQ:a * n + b * m == gcd n m
(q | p * sgn p * (b * m))
 rewrite mul_shuffle2.n, m, p, q:t
H:(q | p * n)
H':(q | p * m)
a, b:t
EQ:a * n + b * m == gcd n m
(q | p * n * (sgn p * a))
n, m, p, q:t
H:(q | p * n)
H':(q | p * m)
a, b:t
EQ:a * n + b * m == gcd n m
(q | p * sgn p * (b * m)) now apply divide_mul_l.n, m, p, q:t
H:(q | p * n)
H':(q | p * m)
a, b:t
EQ:a * n + b * m == gcd n m
(q | p * sgn p * (b * m))
 rewrite mul_shuffle2.n, m, p, q:t
H:(q | p * n)
H':(q | p * m)
a, b:t
EQ:a * n + b * m == gcd n m
(q | p * m * (sgn p * b)) now apply divide_mul_l.
Qed.

Lemma gcd_mul_mono_l_nonneg :
 forall n m p, 0<=p -> gcd (p*n) (p*m) == p * gcd n m.forall n m p : t,
0 <= p -> gcd (p * n) (p * m) == p * gcd n m
Proof.forall n m p : t,
0 <= p -> gcd (p * n) (p * m) == p * gcd n m
 intros.n, m, p:t
H:0 <= p
gcd (p * n) (p * m) == p * gcd n m rewrite <- (abs_eq p) at 3; trivial.n, m, p:t
H:0 <= p
gcd (p * n) (p * m) == abs p * gcd n m apply gcd_mul_mono_l.
Qed.

Lemma gcd_mul_mono_r :
 forall n m p, gcd (n * p) (m * p) == gcd n m * abs p.forall n m p : t,
gcd (n * p) (m * p) == gcd n m * abs p
Proof.forall n m p : t,
gcd (n * p) (m * p) == gcd n m * abs p
 intros n m p.n, m, p:t
gcd (n * p) (m * p) == gcd n m * abs p now rewrite !(mul_comm _ p), gcd_mul_mono_l, mul_comm.
Qed.

Lemma gcd_mul_mono_r_nonneg :
 forall n m p, 0<=p -> gcd (n*p) (m*p) == gcd n m * p.forall n m p : t,
0 <= p -> gcd (n * p) (m * p) == gcd n m * p
Proof.forall n m p : t,
0 <= p -> gcd (n * p) (m * p) == gcd n m * p
 intros.n, m, p:t
H:0 <= p
gcd (n * p) (m * p) == gcd n m * p rewrite <- (abs_eq p) at 3; trivial.n, m, p:t
H:0 <= p
gcd (n * p) (m * p) == gcd n m * abs p apply gcd_mul_mono_r.
Qed.

Lemma gauss : forall n m p, (n | m * p) -> gcd n m == 1 -> (n | p).forall n m p : t,
(n | m * p) -> gcd n m == 1 -> (n | p)
Proof.forall n m p : t,
(n | m * p) -> gcd n m == 1 -> (n | p)
 intros n m p H G.n, m, p:t
H:(n | m * p)
G:gcd n m == 1
(n | p)
 destruct (gcd_bezout n m 1 G) as (a & b & EQ).n, m, p:t
H:(n | m * p)
G:gcd n m == 1
a, b:t
EQ:a * n + b * m == 1
(n | p)
 rewrite <- (mul_1_l p), <- EQ, mul_add_distr_r.n, m, p:t
H:(n | m * p)
G:gcd n m == 1
a, b:t
EQ:a * n + b * m == 1
(n | a * n * p + b * m * p)
 apply divide_add_r.n, m, p:t
H:(n | m * p)
G:gcd n m == 1
a, b:t
EQ:a * n + b * m == 1
(n | a * n * p)
n, m, p:t
H:(n | m * p)
G:gcd n m == 1
a, b:t
EQ:a * n + b * m == 1
(n | b * m * p) rewrite mul_shuffle0.n, m, p:t
H:(n | m * p)
G:gcd n m == 1
a, b:t
EQ:a * n + b * m == 1
(n | a * p * n)
n, m, p:t
H:(n | m * p)
G:gcd n m == 1
a, b:t
EQ:a * n + b * m == 1
(n | b * m * p) apply divide_factor_r.n, m, p:t
H:(n | m * p)
G:gcd n m == 1
a, b:t
EQ:a * n + b * m == 1
(n | b * m * p)
 rewrite <- mul_assoc.n, m, p:t
H:(n | m * p)
G:gcd n m == 1
a, b:t
EQ:a * n + b * m == 1
(n | b * (m * p)) now apply divide_mul_r.
Qed.

Lemma divide_mul_split : forall n m p, n ~= 0 -> (n | m * p) ->
 exists q r, n == q*r /\ (q | m) /\ (r | p).forall n m p : t,
n ~= 0 ->
(n | m * p) ->
exists q r : t, n == q * r /\ (q | m) /\ (r | p)
Proof.forall n m p : t,
n ~= 0 ->
(n | m * p) ->
exists q r : t, n == q * r /\ (q | m) /\ (r | p)
 intros n m p Hn H.n, m, p:t
Hn:n ~= 0
H:(n | m * p)
exists q r : t, n == q * r /\ (q | m) /\ (r | p)
 assert (G := gcd_nonneg n m).n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:0 <= gcd n m
exists q r : t, n == q * r /\ (q | m) /\ (r | p)
 apply le_lteq in G; destruct G as [G|G].n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:0 < gcd n m
exists q r : t, n == q * r /\ (q | m) /\ (r | p)
n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:0 == gcd n m
exists q r : t, n == q * r /\ (q | m) /\ (r | p)
 destruct (gcd_divide_l n m) as (q,Hq).n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:0 < gcd n m
q:t
Hq:n == q * gcd n m
exists q0 r : t, n == q0 * r /\ (q0 | m) /\ (r | p)
n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:0 == gcd n m
exists q r : t, n == q * r /\ (q | m) /\ (r | p)
 exists (gcd n m).n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:0 < gcd n m
q:t
Hq:n == q * gcd n m
exists r : t,
  n == gcd n m * r /\ (gcd n m | m) /\ (r | p)
n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:0 == gcd n m
exists q r : t, n == q * r /\ (q | m) /\ (r | p) exists q.n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:0 < gcd n m
q:t
Hq:n == q * gcd n m
n == gcd n m * q /\ (gcd n m | m) /\ (q | p)
n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:0 == gcd n m
exists q r : t, n == q * r /\ (q | m) /\ (r | p)
 split.n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:0 < gcd n m
q:t
Hq:n == q * gcd n m
n == gcd n m * q
n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:0 < gcd n m
q:t
Hq:n == q * gcd n m
(gcd n m | m) /\ (q | p)
n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:0 == gcd n m
exists q r : t, n == q * r /\ (q | m) /\ (r | p) now rewrite mul_comm.n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:0 < gcd n m
q:t
Hq:n == q * gcd n m
(gcd n m | m) /\ (q | p)
n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:0 == gcd n m
exists q r : t, n == q * r /\ (q | m) /\ (r | p)
 split.n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:0 < gcd n m
q:t
Hq:n == q * gcd n m
(gcd n m | m)
n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:0 < gcd n m
q:t
Hq:n == q * gcd n m
(q | p)
n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:0 == gcd n m
exists q r : t, n == q * r /\ (q | m) /\ (r | p) apply gcd_divide_r.n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:0 < gcd n m
q:t
Hq:n == q * gcd n m
(q | p)
n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:0 == gcd n m
exists q r : t, n == q * r /\ (q | m) /\ (r | p)
 destruct (gcd_divide_r n m) as (r,Hr).n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:0 < gcd n m
q:t
Hq:n == q * gcd n m
r:t
Hr:m == r * gcd n m
(q | p)
n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:0 == gcd n m
exists q r : t, n == q * r /\ (q | m) /\ (r | p)
 rewrite Hr in H.n, m, p:t
Hn:n ~= 0
G:0 < gcd n m
q:t
Hq:n == q * gcd n m
r:t
H:(n | r * gcd n m * p)
Hr:m == r * gcd n m
(q | p)
n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:0 == gcd n m
exists q r : t, n == q * r /\ (q | m) /\ (r | p) rewrite Hq in H at 1.n, m, p:t
Hn:n ~= 0
G:0 < gcd n m
q:t
Hq:n == q * gcd n m
r:t
H:(q * gcd n m | r * gcd n m * p)
Hr:m == r * gcd n m
(q | p)
n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:0 == gcd n m
exists q r : t, n == q * r /\ (q | m) /\ (r | p)
 rewrite mul_shuffle0 in H.n, m, p:t
Hn:n ~= 0
G:0 < gcd n m
q:t
Hq:n == q * gcd n m
r:t
H:(q * gcd n m | r * p * gcd n m)
Hr:m == r * gcd n m
(q | p)
n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:0 == gcd n m
exists q r : t, n == q * r /\ (q | m) /\ (r | p) apply mul_divide_cancel_r in H; [|order].n, m, p:t
Hn:n ~= 0
G:0 < gcd n m
q:t
Hq:n == q * gcd n m
r:t
H:(q | r * p)
Hr:m == r * gcd n m
(q | p)
n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:0 == gcd n m
exists q r : t, n == q * r /\ (q | m) /\ (r | p)
 apply gauss with r; trivial.n, m, p:t
Hn:n ~= 0
G:0 < gcd n m
q:t
Hq:n == q * gcd n m
r:t
H:(q | r * p)
Hr:m == r * gcd n m
gcd q r == 1
n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:0 == gcd n m
exists q r : t, n == q * r /\ (q | m) /\ (r | p)
 apply mul_cancel_r with (gcd n m); [order|].n, m, p:t
Hn:n ~= 0
G:0 < gcd n m
q:t
Hq:n == q * gcd n m
r:t
H:(q | r * p)
Hr:m == r * gcd n m
gcd q r * gcd n m == 1 * gcd n m
n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:0 == gcd n m
exists q r : t, n == q * r /\ (q | m) /\ (r | p)
 rewrite mul_1_l.n, m, p:t
Hn:n ~= 0
G:0 < gcd n m
q:t
Hq:n == q * gcd n m
r:t
H:(q | r * p)
Hr:m == r * gcd n m
gcd q r * gcd n m == gcd n m
n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:0 == gcd n m
exists q r : t, n == q * r /\ (q | m) /\ (r | p)
 rewrite <- gcd_mul_mono_r_nonneg, <- Hq, <- Hr; order.n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:0 == gcd n m
exists q r : t, n == q * r /\ (q | m) /\ (r | p)
 symmetry in G.n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:gcd n m == 0
exists q r : t, n == q * r /\ (q | m) /\ (r | p) apply gcd_eq_0 in G.n, m, p:t
Hn:n ~= 0
H:(n | m * p)
G:n == 0 /\ m == 0
exists q r : t, n == q * r /\ (q | m) /\ (r | p) destruct G as (Hn',_); order.
Qed.

TODO : more about rel_prime (i.e. gcd == 1), about prime ...

End ZGcdProp.