# Library Coq.Numbers.NatInt.NZGcd

Greatest Common Divisor
Require Import NZAxioms NZMulOrder.
Interface of a gcd function, then its specification on naturals
Module Type Gcd (Import A : Typ).
Parameter Inline gcd : t -> t -> t.
End Gcd.
Module Type NZGcdSpec (A : NZOrdAxiomsSig')(B : Gcd A).
Import A B.
Definition divide n m := exists p , m == p * n.
Local Notation "( n | m )" := (divide n m) (at level 0).
Axiom gcd_divide_l : forall n m, ( gcd n m | n ).
Axiom gcd_divide_r : forall n m, ( gcd n m | m ).
Axiom gcd_greatest : forall n m p, ( p | n ) -> ( p | m ) -> ( p | gcd n m ).
Axiom gcd_nonneg : forall n m, 0 <= gcd n m.
End NZGcdSpec.
Module Type DivideNotation (A:NZOrdAxiomsSig')(B:Gcd A)(C:NZGcdSpec A B).
Import A B C.
Notation "( n | m )" := (divide n m) (at level 0).
End DivideNotation.
Module Type NZGcd (A : NZOrdAxiomsSig) := Gcd A <+ NZGcdSpec A.
Module Type NZGcd' (A : NZOrdAxiomsSig) :=
Gcd A <+ NZGcdSpec A <+ DivideNotation A.
Derived properties of gcd
Module NZGcdProp
(Import A : NZOrdAxiomsSig')
(Import B : NZGcd' A)
(Import C : NZMulOrderProp A).
Results concerning divisibility
Instance divide_wd : Proper (eq ==> eq ==> iff) divide.
Lemma divide_1_l : forall n, (1 | n ).
Lemma divide_0_r : forall n, ( n | 0).
Hint Rewrite divide_1_l divide_0_r : nz.
Lemma divide_0_l : forall n, (0 | n ) -> n ==0.
Lemma eq_mul_1_nonneg : forall n m,
0<= n -> n * m == 1 -> n ==1 /\ m ==1.
Lemma eq_mul_1_nonneg' : forall n m,
0<= m -> n * m == 1 -> n ==1 /\ m ==1.
Lemma divide_1_r_nonneg : forall n, 0<= n -> ( n | 1) -> n ==1.
Lemma divide_refl : forall n, ( n | n ).
Lemma divide_trans : forall n m p, ( n | m ) -> ( m | p ) -> ( n | p ).
Instance divide_reflexive : Reflexive divide := divide_refl.
Instance divide_transitive : Transitive divide := divide_trans.
Due to sign, no general antisymmetry result
Lemma divide_antisym_nonneg : forall n m,
0<= n -> 0<= m -> ( n | m ) -> ( m | n ) -> n == m.
Lemma mul_divide_mono_l : forall n m p, ( n | m ) -> ( p * n | p * m ).
Lemma mul_divide_mono_r : forall n m p, ( n | m ) -> ( n * p | m * p ).
Lemma mul_divide_cancel_l : forall n m p, p ~= 0 ->
(( p * n | p * m ) <-> ( n | m )).
Lemma mul_divide_cancel_r : forall n m p, p ~= 0 ->
(( n * p | m * p ) <-> ( n | m )).
Lemma divide_add_r : forall n m p, ( n | m ) -> ( n | p ) -> ( n | m + p ).
Lemma divide_mul_l : forall n m p, ( n | m ) -> ( n | m * p ).
Lemma divide_mul_r : forall n m p, ( n | p ) -> ( n | m * p ).
Lemma divide_factor_l : forall n m, ( n | n * m ).
Lemma divide_factor_r : forall n m, ( n | m * n ).
Lemma divide_pos_le : forall n m, 0 < m -> ( n | m ) -> n <= m.
Basic properties of gcd
Lemma gcd_unique : forall n m p,
0<= p -> ( p | n ) -> ( p | m ) ->
(forall q, ( q | n ) -> ( q | m ) -> ( q | p )) ->
gcd n m == p.
Instance gcd_wd : Proper (eq ==> eq ==> eq) gcd.
Lemma gcd_divide_iff : forall n m p,
( p | gcd n m ) <-> ( p | n ) /\ ( p | m ).
Lemma gcd_unique_alt : forall n m p, 0<= p ->
(forall q, ( q | p ) <-> ( q | n ) /\ ( q | m )) ->
gcd n m == p.
Lemma gcd_comm : forall n m, gcd n m == gcd m n.
Lemma gcd_assoc : forall n m p, gcd n (gcd m p) == gcd (gcd n m) p.
Lemma gcd_0_l_nonneg : forall n, 0<= n -> gcd 0 n == n.
Lemma gcd_0_r_nonneg : forall n, 0<= n -> gcd n 0 == n.
Lemma gcd_1_l : forall n, gcd 1 n == 1.
Lemma gcd_1_r : forall n, gcd n 1 == 1.
Lemma gcd_diag_nonneg : forall n, 0<= n -> gcd n n == n.
Lemma gcd_eq_0_l : forall n m, gcd n m == 0 -> n == 0.
Lemma gcd_eq_0_r : forall n m, gcd n m == 0 -> m == 0.
Lemma gcd_eq_0 : forall n m, gcd n m == 0 <-> n == 0 /\ m == 0.
Lemma gcd_mul_diag_l : forall n m, 0<= n -> gcd n (n * m) == n.
Lemma divide_gcd_iff : forall n m, 0<= n -> (( n | m ) <-> gcd n m == n).
End NZGcdProp.