# Library Coq.ZArith.ZOdiv_def

Require Import BinPos BinNat Nnat ZArith_base.

Open Scope Z_scope.

Definition NPgeb (a:N)(b:positive) :=
match a with
| N0 => false
| Npos na => match Pcompare na b Eq with Lt => false | _ => true end
end.

Fixpoint Pdiv_eucl (a b:positive) : N * N :=
match a with
| xH =>
match b with xH => (1, 0)%N | _ => (0, 1)%N end
| xO a' =>
let (q, r) := Pdiv_eucl a' b in
let r' := (2 * r)%N in
if (NPgeb r' b) then (2 * q + 1, (Nminus r' (Npos b)))%N
else (2 * q, r')%N
| xI a' =>
let (q, r) := Pdiv_eucl a' b in
let r' := (2 * r + 1)%N in
if (NPgeb r' b) then (2 * q + 1, (Nminus r' (Npos b)))%N
else (2 * q, r')%N
end.

Definition ZOdiv_eucl (a b:Z) : Z * Z :=
match a, b with
| Z0, _ => (Z0, Z0)
| _, Z0 => (Z0, a)
| Zpos na, Zpos nb =>
let (nq, nr) := Pdiv_eucl na nb in
(Z_of_N nq, Z_of_N nr)
| Zneg na, Zpos nb =>
let (nq, nr) := Pdiv_eucl na nb in
(Zopp (Z_of_N nq), Zopp (Z_of_N nr))
| Zpos na, Zneg nb =>
let (nq, nr) := Pdiv_eucl na nb in
(Zopp (Z_of_N nq), Z_of_N nr)
| Zneg na, Zneg nb =>
let (nq, nr) := Pdiv_eucl na nb in
(Z_of_N nq, Zopp (Z_of_N nr))
end.

Definition ZOdiv a b := fst (ZOdiv_eucl a b).
Definition ZOmod a b := snd (ZOdiv_eucl a b).

Definition Ndiv_eucl (a b:N) : N * N :=
match a, b with
| N0, _ => (N0, N0)
| _, N0 => (N0, a)
| Npos na, Npos nb => Pdiv_eucl na nb
end.

Definition Ndiv a b := fst (Ndiv_eucl a b).
Definition Nmod a b := snd (Ndiv_eucl a b).

Theorem NPgeb_correct: forall (a:N)(b:positive),
if NPgeb a b then a = (Nminus a (Npos b) + Npos b)%N else True.

Hint Rewrite Z_of_N_plus Z_of_N_mult Z_of_N_minus Zmult_1_l Zmult_assoc
Zmult_plus_distr_l Zmult_plus_distr_r : zdiv.
Hint Rewrite <- Zplus_assoc : zdiv.

Theorem Pdiv_eucl_correct: forall a b,
let (q,r) := Pdiv_eucl a b in
Zpos a = Z_of_N q * Zpos b + Z_of_N r.

Theorem ZOdiv_eucl_correct: forall a b,
let (q,r) := ZOdiv_eucl a b in a = q * b + r.

Theorem Ndiv_eucl_correct: forall a b,
let (q,r) := Ndiv_eucl a b in a = (q * b + r)%N.