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).
Module Import Private_NZGcdProp := NZGcdProp A A B.
Properties of divide
#[global] Instance divide_wd : Proper (eq==>eq==>iff) divide := divide_wd.
Definition divide_1_r n := divide_1_r_nonneg n (le_0_l n).
Definition divide_1_l := divide_1_l.
Definition divide_0_r := divide_0_r.
Definition divide_0_l := divide_0_l.
Definition divide_refl := divide_refl.
Definition divide_trans := divide_trans.
#[global] Instance divide_reflexive : Reflexive divide | 5 := divide_refl.
#[global] Instance divide_transitive : Transitive divide | 5 := divide_trans.
Definition divide_antisym n m := divide_antisym_nonneg n m (le_0_l n) (le_0_l m).
Definition mul_divide_mono_l := mul_divide_mono_l.
Definition mul_divide_mono_r := mul_divide_mono_r.
Definition mul_divide_cancel_l := mul_divide_cancel_l.
Definition mul_divide_cancel_r := mul_divide_cancel_r.
Definition divide_add_r := divide_add_r.
Definition divide_mul_l := divide_mul_l.
Definition divide_mul_r := divide_mul_r.
Definition divide_factor_l := divide_factor_l.
Definition divide_factor_r := divide_factor_r.
Definition divide_pos_le := divide_pos_le.
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).
#[global] Instance gcd_wd : Proper (eq==>eq==>eq) gcd := gcd_wd.
Definition gcd_comm := gcd_comm.
Definition gcd_assoc := gcd_assoc.
Definition gcd_eq_0_l := gcd_eq_0_l.
Definition gcd_eq_0_r := gcd_eq_0_r.
Definition gcd_eq_0 := gcd_eq_0.
Definition gcd_mul_diag_l n m := gcd_mul_diag_l n m (le_0_l n).
#[deprecated(since="8.17",note="Use divide_antisym instead.")]
Notation divide_antisym_nonneg := divide_antisym_nonneg (only parsing).
#[deprecated(since="8.17",note="Use gcd_unique instead.")]
Notation gcd_unique' n m p := gcd_unique (only parsing).
#[deprecated(since="8.17",note="Use gcd_unique_alt instead.")]
Notation gcd_unique_alt' := gcd_unique_alt.
#[deprecated(since="8.17",note="Use divide_gcd_iff instead.")]
Notation divide_gcd_iff' := divide_gcd_iff.
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).
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.
#[global]
Instance Bezout_wd : Proper (eq==>eq==>eq==>iff) Bezout.
Lemma bezout_1_gcd : forall n m, Bezout n m 1 -> gcd n m == 1.
Bezout on natural numbers commutes
Theorem bezout_comm : forall a b g,
b ~= 0 -> Bezout a b g -> Bezout b a g.
Lemma gcd_bezout_pos : forall n m, 0 < n -> Bezout n m (gcd n m).
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).
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 ...