Library Coq.Numbers.Natural.Abstract.NGcd

Require Import NAxioms NSub NZGcd.

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

 Include NZGcdProp A A B.

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).

Lemma divide_sub_r : forall n m p, (n | m) -> (n | p) -> (n | m - p).

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.

Lemma gcd_add_diag_r : forall n m, gcd n (m+n) == gcd n m.

Lemma gcd_sub_diag_r : forall n m, n<=m -> gcd n (m-n) == gcd n m.

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

Instance Bezout_wd : Proper (eq==>eq==>eq==>iff) Bezout.

Lemma bezout_1_gcd : forall n m, Bezout n m 1 -> gcd n m == 1.

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).

Lemma gcd_bezout_pos : forall n m, 0<n -> Bezout n m (gcd n m).

Lemma gcd_bezout : forall n m,
 Bezout n m (gcd n m) \/ Bezout m n (gcd n m).

Lemma gcd_mul_mono_l :
  forall n m p, gcd (p * n) (p * m) == p * gcd n m.

Lemma gcd_mul_mono_r :
 forall n m p, gcd (n*p) (m*p) == gcd n m * p.

Lemma gauss : forall n m p, (n | m * p) -> gcd n m == 1 -> (n | p).

Lemma divide_mul_split : forall n m p, n ~= 0 -> (n | m * p) ->
 exists q r, n == q*r /\ (q | m) /\ (r | p).

End NGcdProp.