Library Coq.Numbers.Integer.Abstract.ZGcd

Require Import ZAxioms ZMulOrder ZSgnAbs NZGcd.

Module Type ZGcdProp
 (Import A : ZAxiomsSig')
 (Import B : ZMulOrderProp A)
 (Import C : ZSgnAbsProp A B).

 Include NZGcdProp A A B.

Lemma divide_opp_l : forall n m, (-n | m) <-> (n | m).

Lemma divide_opp_r : forall n m, (n | -m) <-> (n | m).

Lemma divide_abs_l : forall n m, (abs n | m) <-> (n | m).

Lemma divide_abs_r : forall n m, (n | abs m) <-> (n | m).

Lemma divide_1_r_abs : forall n, (n | 1) -> abs n == 1.

Lemma divide_1_r : forall n, (n | 1) -> n==1 \/ n==-1.

Lemma divide_antisym_abs : forall n m,
 (n | m) -> (m | n) -> abs n == abs m.

Lemma divide_antisym : forall n m,
 (n | m) -> (m | n) -> n == m \/ n == -m.

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

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

Lemma gcd_opp_l : forall n m, gcd (-n) m == gcd n m.

Lemma gcd_opp_r : forall n m, gcd n (-m) == gcd n m.

Lemma gcd_abs_l : forall n m, gcd (abs n) m == gcd n m.

Lemma gcd_abs_r : forall n m, gcd n (abs m) == gcd n m.

Lemma gcd_0_l : forall n, gcd 0 n == abs n.

Lemma gcd_0_r : forall n, gcd n 0 == abs n.

Lemma gcd_diag : forall n, gcd n n == abs 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, gcd n (m-n) == gcd n m.

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

#[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.

Lemma gcd_bezout : forall n m p, gcd n m == p -> Bezout n m p.

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

Lemma gcd_mul_mono_l_nonneg :
 forall n m p, 0<=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 * abs p.

Lemma gcd_mul_mono_r_nonneg :
 forall n m p, 0<=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 ZGcdProp.