# Library Coq.Numbers.Natural.Abstract.NGcd

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 ).
Lemma divide_sub_r : forall n m p, ( n | m ) -> ( n | p ) -> ( n | m - p ).
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.
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.
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.
Lemma bezout_1_gcd : forall n m, Bezout n m 1 -> gcd n m == 1.
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).
Lemma gcd_bezout_pos : forall n m, 0< n -> Bezout n m (gcd n m).
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).
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 ).
TODO : relation between gcd and division and modulo
TODO : more about rel_prime (i.e. gcd == 1), about prime ...
End NGcdProp.