NGcd.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 NAxioms NSub NZGcd.

Module Type NGcdProp
 (Import A : NAxiomsSig')
 (Import B : NSubProp A).

 Include NZGcdProp A A B.

Results concerning divisibility

Definition divide_1_r n : (n | 1) -> n == 1
 := divide_1_r_nonneg n (le_0_l n).

Definition divide_antisym n m : (n | m) -> (m | n) -> n == m
 := divide_antisym_nonneg n m (le_0_l n) (le_0_l m).

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 (q,Hq) (r,Hr).n, m, p, q:t
Hq:m == q * n
r:t
Hr:m + p == r * n
(n | p)
 exists (r-q).n, m, p, q:t
Hq:m == q * n
r:t
Hr:m + p == r * n
p == (r - q) * n rewrite mul_sub_distr_r, <- Hq, <- Hr.n, m, p, q:t
Hq:m == q * n
r:t
Hr:m + p == r * n
p == m + p - m
 now rewrite add_comm, add_sub.
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)
 destruct (le_ge_cases m p) as [LE|LE].n, m, p:t
H:(n | m)
H':(n | p)
LE:m <= p
(n | m - p)
n, m, p:t
H:(n | m)
H':(n | p)
LE:p <= m
(n | m - p)
 apply sub_0_le in LE.n, m, p:t
H:(n | m)
H':(n | p)
LE:m - p == 0
(n | m - p)
n, m, p:t
H:(n | m)
H':(n | p)
LE:p <= m
(n | m - p) rewrite LE.n, m, p:t
H:(n | m)
H':(n | p)
LE:m - p == 0
(n | 0)
n, m, p:t
H:(n | m)
H':(n | p)
LE:p <= m
(n | m - p) apply divide_0_r.n, m, p:t
H:(n | m)
H':(n | p)
LE:p <= m
(n | m - p)
 apply divide_add_cancel_r with p; trivial.n, m, p:t
H:(n | m)
H':(n | p)
LE:p <= m
(n | p + (m - p))
 now rewrite add_comm, sub_add.
Qed.

Properties of gcd

Definition gcd_0_l n : gcd 0 n == n := gcd_0_l_nonneg n (le_0_l n).
Definition gcd_0_r n : gcd n 0 == n := gcd_0_r_nonneg n (le_0_l n).
Definition gcd_diag n : gcd n n == n := gcd_diag_nonneg n (le_0_l n).
Definition gcd_unique' n m p := gcd_unique n m p (le_0_l p).
Definition gcd_unique_alt' n m p := gcd_unique_alt n m p (le_0_l p).
Definition divide_gcd_iff' n m := divide_gcd_iff n m (le_0_l n).

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'.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, n<=m -> gcd n (m-n) == gcd n m.forall n m : t, n <= m -> gcd n (m - n) == gcd n m
Proof.forall n m : t, n <= m -> gcd n (m - n) == gcd n m
 intros n m H.n, m:t
H:n <= m
gcd n (m - n) == gcd n m symmetry.n, m:t
H:n <= m
gcd n m == gcd n (m - n)
 rewrite <- (sub_add n m H) at 1.n, m:t
H:n <= m
gcd n (m - n + n) == gcd n (m - n) apply gcd_add_diag_r.
Qed.

On natural numbers, we should use a particular form for the Bezout identity, since we don't have full subtraction.

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

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 == p + b * m) 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 == z + b * y) <->
(exists a b : t, a * x' == z' + b * y')
 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' == z + b * y) <->
(exists a b : t, a * x' == z' + b * y') 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' == z + b * y') <->
(exists a b : t, a * x' == z' + b * y') 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 == 1 + r * m
gcd n m == 1
 apply gcd_unique; trivial using divide_1_l, le_0_1.n, m, q, r:t
H:q * n == 1 + r * m
forall q0 : t, (q0 | n) -> (q0 | m) -> (q0 | 1)
 intros p Hn Hm.n, m, q, r:t
H:q * n == 1 + r * m
p:t
Hn:(p | n)
Hm:(p | m)
(p | 1)
 apply divide_add_cancel_r with (r*m).n, m, q, r:t
H:q * n == 1 + r * m
p:t
Hn:(p | n)
Hm:(p | m)
(p | r * m)
n, m, q, r:t
H:q * n == 1 + r * m
p:t
Hn:(p | n)
Hm:(p | m)
(p | r * m + 1)
 now apply divide_mul_r.n, m, q, r:t
H:q * n == 1 + r * m
p:t
Hn:(p | n)
Hm:(p | m)
(p | r * m + 1)
 rewrite add_comm, <- H.n, m, q, r:t
H:q * n == 1 + r * m
p:t
Hn:(p | n)
Hm:(p | m)
(p | q * n) now apply divide_mul_r.
Qed.

For strictly positive numbers, we have Bezout in the two directions.

Lemma gcd_bezout_pos_pos : forall n, 0<n -> forall m, 0<m ->
 Bezout n m (gcd n m) /\ Bezout m n (gcd n m).forall n : t,
0 < n ->
forall m : t,
0 < m -> Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
Proof.forall n : t,
0 < n ->
forall m : t,
0 < m -> Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
 intros n Hn.n:t
Hn:0 < n
forall m : t,
0 < m -> Bezout n m (gcd n m) /\ Bezout m n (gcd n m) rewrite <- le_succ_l, <- one_succ in Hn.n:t
Hn:1 <= n
forall m : t,
0 < m -> Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
 pattern n.n:t
Hn:1 <= n
(fun t0 : t =>
 forall m : t,
 0 < m ->
 Bezout t0 m (gcd t0 m) /\ Bezout m t0 (gcd t0 m)) n apply strong_right_induction with (z:=1); trivial.n:t
Hn:1 <= n
Proper (eq ==> iff)
  (fun t0 : t =>
   forall m : t,
   0 < m ->
   Bezout t0 m (gcd t0 m) /\ Bezout m t0 (gcd t0 m))
n:t
Hn:1 <= n
forall n0 : t,
1 <= n0 ->
(forall m : t,
 1 <= m ->
 m < n0 ->
 forall m0 : t,
 0 < m0 ->
 Bezout m m0 (gcd m m0) /\ Bezout m0 m (gcd m m0)) ->
forall m : t,
0 < m ->
Bezout n0 m (gcd n0 m) /\ Bezout m n0 (gcd n0 m)
 unfold Bezout.n:t
Hn:1 <= n
Proper (eq ==> iff)
  (fun t0 : t =>
   forall m : t,
   0 < m ->
   (exists a b : t, a * t0 == gcd t0 m + b * m) /\
   (exists a b : t, a * m == gcd t0 m + b * t0))
n:t
Hn:1 <= n
forall n0 : t,
1 <= n0 ->
(forall m : t,
 1 <= m ->
 m < n0 ->
 forall m0 : t,
 0 < m0 ->
 Bezout m m0 (gcd m m0) /\ Bezout m0 m (gcd m m0)) ->
forall m : t,
0 < m ->
Bezout n0 m (gcd n0 m) /\ Bezout m n0 (gcd n0 m) solve_proper.n:t
Hn:1 <= n
forall n0 : t,
1 <= n0 ->
(forall m : t,
 1 <= m ->
 m < n0 ->
 forall m0 : t,
 0 < m0 ->
 Bezout m m0 (gcd m m0) /\ Bezout m0 m (gcd m m0)) ->
forall m : t,
0 < m ->
Bezout n0 m (gcd n0 m) /\ Bezout m n0 (gcd n0 m)
 clear n Hn.forall n : t,
1 <= n ->
(forall m : t,
 1 <= m ->
 m < n ->
 forall m0 : t,
 0 < m0 ->
 Bezout m m0 (gcd m m0) /\ Bezout m0 m (gcd m m0)) ->
forall m : t,
0 < m -> Bezout n m (gcd n m) /\ Bezout m n (gcd n m) intros n Hn IHn.n:t
Hn:1 <= n
IHn:forall m : t,
1 <= m ->
m < n ->
forall m0 : t, 0 < m0 -> Bezout m m0 (gcd m m0) /\ Bezout m0 m (gcd m m0)
forall m : t,
0 < m -> Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
 intros m Hm.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:0 < m
Bezout n m (gcd n m) /\ Bezout m n (gcd n m) rewrite <- le_succ_l, <- one_succ in Hm.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
 pattern m.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
(fun t0 : t =>
 Bezout n t0 (gcd n t0) /\ Bezout t0 n (gcd n t0)) m apply strong_right_induction with (z:=1); trivial.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
Proper (eq ==> iff)
  (fun t0 : t =>
   Bezout n t0 (gcd n t0) /\ Bezout t0 n (gcd n t0))
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
forall n0 : t,
1 <= n0 ->
(forall m0 : t,
 1 <= m0 ->
 m0 < n0 ->
 Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)) ->
Bezout n n0 (gcd n n0) /\ Bezout n0 n (gcd n n0)
 unfold Bezout.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
Proper (eq ==> iff)
  (fun t0 : t =>
   (exists a b : t, a * n == gcd n t0 + b * t0) /\
   (exists a b : t, a * t0 == gcd n t0 + b * n))
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
forall n0 : t,
1 <= n0 ->
(forall m0 : t,
 1 <= m0 ->
 m0 < n0 ->
 Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)) ->
Bezout n n0 (gcd n n0) /\ Bezout n0 n (gcd n n0) solve_proper.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
forall n0 : t,
1 <= n0 ->
(forall m0 : t,
 1 <= m0 ->
 m0 < n0 ->
 Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)) ->
Bezout n n0 (gcd n n0) /\ Bezout n0 n (gcd n n0)
 clear m Hm.n:t
Hn:1 <= n
IHn:forall m : t,
1 <= m ->
m < n ->
forall m0 : t, 0 < m0 -> Bezout m m0 (gcd m m0) /\ Bezout m0 m (gcd m m0)
forall n0 : t,
1 <= n0 ->
(forall m : t,
 1 <= m ->
 m < n0 ->
 Bezout n m (gcd n m) /\ Bezout m n (gcd n m)) ->
Bezout n n0 (gcd n n0) /\ Bezout n0 n (gcd n n0) intros m Hm IHm.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
 destruct (lt_trichotomy n m) as [LT|[EQ|LT]].n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
 (* n < m *)
 destruct (IHm (m-n)) as ((a & b & EQ), (a' & b' & EQ')).n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
1 <= m - n
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
m - n < m
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
a, b:t
EQ:a * n == gcd n (m - n) + b * (m - n)
a', b':t
EQ':a' * (m - n) == gcd n (m - n) + b' * n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
 rewrite one_succ, le_succ_l.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
0 < m - n
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
m - n < m
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
a, b:t
EQ:a * n == gcd n (m - n) + b * (m - n)
a', b':t
EQ':a' * (m - n) == gcd n (m - n) + b' * n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
 apply lt_add_lt_sub_l; now nzsimpl.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
m - n < m
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
a, b:t
EQ:a * n == gcd n (m - n) + b * (m - n)
a', b':t
EQ':a' * (m - n) == gcd n (m - n) + b' * n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
 apply sub_lt; order'.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
a, b:t
EQ:a * n == gcd n (m - n) + b * (m - n)
a', b':t
EQ':a' * (m - n) == gcd n (m - n) + b' * n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
 split.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
a, b:t
EQ:a * n == gcd n (m - n) + b * (m - n)
a', b':t
EQ':a' * (m - n) == gcd n (m - n) + b' * n
Bezout n m (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
a, b:t
EQ:a * n == gcd n (m - n) + b * (m - n)
a', b':t
EQ':a' * (m - n) == gcd n (m - n) + b' * n
Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
 exists (a+b).n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
a, b:t
EQ:a * n == gcd n (m - n) + b * (m - n)
a', b':t
EQ':a' * (m - n) == gcd n (m - n) + b' * n
exists b0 : t, (a + b) * n == gcd n m + b0 * m
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
a, b:t
EQ:a * n == gcd n (m - n) + b * (m - n)
a', b':t
EQ':a' * (m - n) == gcd n (m - n) + b' * n
Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m) exists b.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
a, b:t
EQ:a * n == gcd n (m - n) + b * (m - n)
a', b':t
EQ':a' * (m - n) == gcd n (m - n) + b' * n
(a + b) * n == gcd n m + b * m
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
a, b:t
EQ:a * n == gcd n (m - n) + b * (m - n)
a', b':t
EQ':a' * (m - n) == gcd n (m - n) + b' * n
Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
 rewrite mul_add_distr_r, EQ, mul_sub_distr_l, <- add_assoc.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
a, b:t
EQ:a * n == gcd n (m - n) + b * (m - n)
a', b':t
EQ':a' * (m - n) == gcd n (m - n) + b' * n
gcd n (m - n) + (b * m - b * n + b * n) ==
gcd n m + b * m
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
a, b:t
EQ:a * n == gcd n (m - n) + b * (m - n)
a', b':t
EQ':a' * (m - n) == gcd n (m - n) + b' * n
Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
 rewrite gcd_sub_diag_r by order.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
a, b:t
EQ:a * n == gcd n (m - n) + b * (m - n)
a', b':t
EQ':a' * (m - n) == gcd n (m - n) + b' * n
gcd n m + (b * m - b * n + b * n) == gcd n m + b * m
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
a, b:t
EQ:a * n == gcd n (m - n) + b * (m - n)
a', b':t
EQ':a' * (m - n) == gcd n (m - n) + b' * n
Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
 rewrite sub_add.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
a, b:t
EQ:a * n == gcd n (m - n) + b * (m - n)
a', b':t
EQ':a' * (m - n) == gcd n (m - n) + b' * n
gcd n m + b * m == gcd n m + b * m
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
a, b:t
EQ:a * n == gcd n (m - n) + b * (m - n)
a', b':t
EQ':a' * (m - n) == gcd n (m - n) + b' * n
b * n <= b * m
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
a, b:t
EQ:a * n == gcd n (m - n) + b * (m - n)
a', b':t
EQ':a' * (m - n) == gcd n (m - n) + b' * n
Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m) reflexivity.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
a, b:t
EQ:a * n == gcd n (m - n) + b * (m - n)
a', b':t
EQ':a' * (m - n) == gcd n (m - n) + b' * n
b * n <= b * m
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
a, b:t
EQ:a * n == gcd n (m - n) + b * (m - n)
a', b':t
EQ':a' * (m - n) == gcd n (m - n) + b' * n
Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m) apply mul_le_mono_l; order.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
a, b:t
EQ:a * n == gcd n (m - n) + b * (m - n)
a', b':t
EQ':a' * (m - n) == gcd n (m - n) + b' * n
Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
 exists a'.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
a, b:t
EQ:a * n == gcd n (m - n) + b * (m - n)
a', b':t
EQ':a' * (m - n) == gcd n (m - n) + b' * n
exists b0 : t, a' * m == gcd n m + b0 * n
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m) exists (a'+b').n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
a, b:t
EQ:a * n == gcd n (m - n) + b * (m - n)
a', b':t
EQ':a' * (m - n) == gcd n (m - n) + b' * n
a' * m == gcd n m + (a' + b') * n
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
 rewrite gcd_sub_diag_r in EQ' by order.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
a, b:t
EQ:a * n == gcd n (m - n) + b * (m - n)
a', b':t
EQ':a' * (m - n) == gcd n m + b' * n
a' * m == gcd n m + (a' + b') * n
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
 rewrite (add_comm a'), mul_add_distr_r, add_assoc, <- EQ'.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
a, b:t
EQ:a * n == gcd n (m - n) + b * (m - n)
a', b':t
EQ':a' * (m - n) == gcd n m + b' * n
a' * m == a' * (m - n) + a' * n
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
 rewrite mul_sub_distr_l, sub_add.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
a, b:t
EQ:a * n == gcd n (m - n) + b * (m - n)
a', b':t
EQ':a' * (m - n) == gcd n m + b' * n
a' * m == a' * m
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
a, b:t
EQ:a * n == gcd n (m - n) + b * (m - n)
a', b':t
EQ':a' * (m - n) == gcd n m + b' * n
a' * n <= a' * m
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m) reflexivity.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:n < m
a, b:t
EQ:a * n == gcd n (m - n) + b * (m - n)
a', b':t
EQ':a' * (m - n) == gcd n m + b' * n
a' * n <= a' * m
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m) apply mul_le_mono_l; order.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
 (* n = m *)
 rewrite EQ.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
Bezout m m (gcd m m) /\ Bezout m m (gcd m m)
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m) rewrite gcd_diag.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
Bezout m m m /\ Bezout m m m
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
 split.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
Bezout m m m
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
Bezout m m m
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
 exists 1.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
exists b : t, 1 * m == m + b * m
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
Bezout m m m
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m) exists 0.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
1 * m == m + 0 * m
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
Bezout m m m
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m) now nzsimpl.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
Bezout m m m
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
 exists 1.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
exists b : t, 1 * m == m + b * m
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m) exists 0.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
EQ:n == m
1 * m == m + 0 * m
n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m) now nzsimpl.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
Bezout n m (gcd n m) /\ Bezout m n (gcd n m)
 (* m < n *)
 rewrite gcd_comm, and_comm.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
Bezout m n (gcd m n) /\ Bezout n m (gcd m n)
 apply IHn; trivial.n:t
Hn:1 <= n
IHn:forall m0 : t,
1 <= m0 ->
m0 < n ->
forall m1 : t, 0 < m1 -> Bezout m0 m1 (gcd m0 m1) /\ Bezout m1 m0 (gcd m0 m1)
m:t
Hm:1 <= m
IHm:forall m0 : t,
1 <= m0 -> m0 < m -> Bezout n m0 (gcd n m0) /\ Bezout m0 n (gcd n m0)
LT:m < n
0 < n
 now rewrite <- le_succ_l, <- one_succ.
Qed.

Lemma gcd_bezout_pos : forall n m, 0<n -> Bezout n m (gcd n m).forall n m : t, 0 < n -> Bezout n m (gcd n m)
Proof.forall n m : t, 0 < n -> Bezout n m (gcd n m)
 intros n m Hn.n, m:t
Hn:0 < n
Bezout n m (gcd n m)
 destruct (eq_0_gt_0_cases m) as [EQ|LT].n, m:t
Hn:0 < n
EQ:m == 0
Bezout n m (gcd n m)
n, m:t
Hn:0 < n
LT:0 < m
Bezout n m (gcd n m)
 rewrite EQ, gcd_0_r.n, m:t
Hn:0 < n
EQ:m == 0
Bezout n 0 n
n, m:t
Hn:0 < n
LT:0 < m
Bezout n m (gcd n m) exists 1.n, m:t
Hn:0 < n
EQ:m == 0
exists b : t, 1 * n == n + b * 0
n, m:t
Hn:0 < n
LT:0 < m
Bezout n m (gcd n m) exists 0.n, m:t
Hn:0 < n
EQ:m == 0
1 * n == n + 0 * 0
n, m:t
Hn:0 < n
LT:0 < m
Bezout n m (gcd n m) now nzsimpl.n, m:t
Hn:0 < n
LT:0 < m
Bezout n m (gcd n m)
 now apply gcd_bezout_pos_pos.
Qed.

For arbitrary natural numbers, we could only say that at least one of the Bezout identities holds.

Lemma gcd_bezout : forall n m,
 Bezout n m (gcd n m) \/ Bezout m n (gcd n m).forall n m : t,
Bezout n m (gcd n m) \/ Bezout m n (gcd n m)
Proof.forall n m : t,
Bezout n m (gcd n m) \/ Bezout m n (gcd n m)
 intros n m.n, m:t
Bezout n m (gcd n m) \/ Bezout m n (gcd n m)
 destruct (eq_0_gt_0_cases n) as [EQ|LT].n, m:t
EQ:n == 0
Bezout n m (gcd n m) \/ Bezout m n (gcd n m)
n, m:t
LT:0 < n
Bezout n m (gcd n m) \/ Bezout m n (gcd n m)
 right.n, m:t
EQ:n == 0
Bezout m n (gcd n m)
n, m:t
LT:0 < n
Bezout n m (gcd n m) \/ Bezout m n (gcd n m) rewrite EQ, gcd_0_l.n, m:t
EQ:n == 0
Bezout m 0 m
n, m:t
LT:0 < n
Bezout n m (gcd n m) \/ Bezout m n (gcd n m) exists 1.n, m:t
EQ:n == 0
exists b : t, 1 * m == m + b * 0
n, m:t
LT:0 < n
Bezout n m (gcd n m) \/ Bezout m n (gcd n m) exists 0.n, m:t
EQ:n == 0
1 * m == m + 0 * 0
n, m:t
LT:0 < n
Bezout n m (gcd n m) \/ Bezout m n (gcd n m) now nzsimpl.n, m:t
LT:0 < n
Bezout n m (gcd n m) \/ Bezout m n (gcd n m)
 left.n, m:t
LT:0 < n
Bezout n m (gcd n m) now apply gcd_bezout_pos.
Qed.

Lemma gcd_mul_mono_l :
  forall n m p, gcd (p * n) (p * m) == p * gcd n m.forall n m p : t, gcd (p * n) (p * m) == p * gcd n m
Proof.forall n m p : t, gcd (p * n) (p * m) == p * gcd n m
 intros n m p.n, m, p:t
gcd (p * n) (p * m) == p * gcd n m
 apply gcd_unique'.n, m, p:t
(p * gcd n m | p * n)
n, m, p:t
(p * gcd n m | p * m)
n, m, p:t
forall q : t,
(q | p * n) -> (q | p * m) -> (q | p * gcd n m)
 apply mul_divide_mono_l, gcd_divide_l.n, m, p:t
(p * gcd n m | p * m)
n, m, p:t
forall q : t,
(q | p * n) -> (q | p * m) -> (q | p * gcd n m)
 apply mul_divide_mono_l, gcd_divide_r.n, m, p:t
forall q : t,
(q | p * n) -> (q | p * m) -> (q | p * gcd n m)
 intros q H H'.n, m, p, q:t
H:(q | p * n)
H':(q | p * m)
(q | p * gcd n m)
 destruct (eq_0_gt_0_cases n) as [EQ|LT].n, m, p, q:t
H:(q | p * n)
H':(q | p * m)
EQ:n == 0
(q | p * gcd n m)
n, m, p, q:t
H:(q | p * n)
H':(q | p * m)
LT:0 < n
(q | p * gcd n m)
 rewrite EQ in *.n, m, p, q:t
H:(q | p * 0)
H':(q | p * m)
EQ:n == 0
(q | p * gcd 0 m)
n, m, p, q:t
H:(q | p * n)
H':(q | p * m)
LT:0 < n
(q | p * gcd n m) now rewrite gcd_0_l.n, m, p, q:t
H:(q | p * n)
H':(q | p * m)
LT:0 < n
(q | p * gcd n m)
 destruct (gcd_bezout_pos n m) as (a & b & EQ); trivial.n, m, p, q:t
H:(q | p * n)
H':(q | p * m)
LT:0 < n
a, b:t
EQ:a * n == gcd n m + b * m
(q | p * gcd n m)
 apply divide_add_cancel_r with (p*m*b).n, m, p, q:t
H:(q | p * n)
H':(q | p * m)
LT:0 < n
a, b:t
EQ:a * n == gcd n m + b * m
(q | p * m * b)
n, m, p, q:t
H:(q | p * n)
H':(q | p * m)
LT:0 < n
a, b:t
EQ:a * n == gcd n m + b * m
(q | p * m * b + p * gcd n m)
 now apply divide_mul_l.n, m, p, q:t
H:(q | p * n)
H':(q | p * m)
LT:0 < n
a, b:t
EQ:a * n == gcd n m + b * m
(q | p * m * b + p * gcd n m)
 rewrite <- mul_assoc, <- mul_add_distr_l, add_comm, (mul_comm m), <- EQ.n, m, p, q:t
H:(q | p * n)
H':(q | p * m)
LT:0 < n
a, b:t
EQ:a * n == gcd n m + b * m
(q | p * (a * n))
 rewrite (mul_comm a), mul_assoc.n, m, p, q:t
H:(q | p * n)
H':(q | p * m)
LT:0 < n
a, b:t
EQ:a * n == gcd n m + b * m
(q | p * n * a)
 now apply divide_mul_l.
Qed.

Lemma gcd_mul_mono_r :
 forall n m p, gcd (n*p) (m*p) == gcd n m * p.forall n m p : t, gcd (n * p) (m * p) == gcd n m * p
Proof.forall n m p : t, gcd (n * p) (m * p) == gcd n m * p
 intros.n, m, p:t
gcd (n * p) (m * p) == gcd n m * p rewrite !(mul_comm _ p).n, m, p:t
gcd (p * n) (p * m) == p * gcd n m apply gcd_mul_mono_l.
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 (eq_0_gt_0_cases n) as [EQ|LT].n, m, p:t
H:(n | m * p)
G:gcd n m == 1
EQ:n == 0
(n | p)
n, m, p:t
H:(n | m * p)
G:gcd n m == 1
LT:0 < n
(n | p)
 rewrite EQ in *.n, m, p:t
H:(0 | m * p)
G:gcd 0 m == 1
EQ:n == 0
(0 | p)
n, m, p:t
H:(n | m * p)
G:gcd n m == 1
LT:0 < n
(n | p) rewrite gcd_0_l in G.n, m, p:t
H:(0 | m * p)
G:m == 1
EQ:n == 0
(0 | p)
n, m, p:t
H:(n | m * p)
G:gcd n m == 1
LT:0 < n
(n | p) now rewrite <- (mul_1_l p), <- G.n, m, p:t
H:(n | m * p)
G:gcd n m == 1
LT:0 < n
(n | p)
 destruct (gcd_bezout_pos n m) as (a & b & EQ); trivial.n, m, p:t
H:(n | m * p)
G:gcd n m == 1
LT:0 < n
a, b:t
EQ:a * n == gcd n m + b * m
(n | p)
 rewrite G in EQ.n, m, p:t
H:(n | m * p)
G:gcd n m == 1
LT:0 < n
a, b:t
EQ:a * n == 1 + b * m
(n | p)
 apply divide_add_cancel_r with (m*p*b).n, m, p:t
H:(n | m * p)
G:gcd n m == 1
LT:0 < n
a, b:t
EQ:a * n == 1 + b * m
(n | m * p * b)
n, m, p:t
H:(n | m * p)
G:gcd n m == 1
LT:0 < n
a, b:t
EQ:a * n == 1 + b * m
(n | m * p * b + p)
 now apply divide_mul_l.n, m, p:t
H:(n | m * p)
G:gcd n m == 1
LT:0 < n
a, b:t
EQ:a * n == 1 + b * m
(n | m * p * b + p)
 rewrite (mul_comm _ b), mul_assoc.n, m, p:t
H:(n | m * p)
G:gcd n m == 1
LT:0 < n
a, b:t
EQ:a * n == 1 + b * m
(n | b * m * p + p) rewrite <- (mul_1_l p) at 2.n, m, p:t
H:(n | m * p)
G:gcd n m == 1
LT:0 < n
a, b:t
EQ:a * n == 1 + b * m
(n | b * m * p + 1 * p)
 rewrite <- mul_add_distr_r, add_comm, <- EQ.n, m, p:t
H:(n | m * p)
G:gcd n m == 1
LT:0 < n
a, b:t
EQ:a * n == 1 + b * m
(n | a * n * p)
 now apply divide_mul_l, divide_factor_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) le_elim 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, <- 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 : relation between gcd and division and modulo

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

End NGcdProp.