# Library aritmo

Require Import Znumtheory.
Require Import ZArith.
Require Import Setoid.
Require Import Ring.
Require Import Omega.

Local Open Scope Z_scope.

Definition Z_zerop (z:Z) : { z = 0 } + { z 0 }.
Defined.

Lemma div_0_is_0 : {a}, (0|a)a = 0.

Lemma plus_div_2 : z, ( z + z ) / 2 = z.

Section Congruence.

Definition congrS n x y := { q : Z | y = x + q × n }.
Definition congr n x y : Prop :=
q, y = x + q × n.

Lemma congr_refl : n x, congr n x x.

Lemma congr_sym : n x y, congr n x ycongr n y x.

Lemma congr_trans n : transitive _ (congr n).

Lemma congr_0_eq : x y, congr 0 x yx = y.

Lemma congr_1 : x y, congr 1 x y.

Lemma congr_divide : n m x y,
congr n x y(m | n)
congr m x y.

Lemma congr_plus_compat_l : n x y m,
congr n x y
congr n (x + m) (y + m).

Lemma congr_minus_compat_l : n x y m,
congr n x y
congr n (x - m) (y - m).

Lemma congr_minus_compat n x y z t :
congr n x y
congr n z t
congr n (x - z) (y - t).

Lemma congr_neg_compat n x y :
congr n x y
congr n (-x) (-y).

Lemma congr_plus_compat : n x y z t,
congr n x ycongr n z t
congr n (x + z) (y + t).

Lemma congr_diff : a b,
congr (a - b) a b.

Lemma congr_mod_compat : n x, n > 0 →
congr n x (x mod n).

Lemma congr_eqm : n x y, n > 0 →
congr n x yeqm n x y.

Lemma eqm_congr : n x y, n > 0 →
eqm n x ycongr n x y.

Lemma congr_mult_l_compat :
n p x y,
congr n x y
congr (p × n) (p × x) (p × y).

Lemma congr_opp n x y :
congr n x y
congr n (-x) (-y).

Definition congr_dec n x y :
{congr n x y} + {¬congr n x y}.

Definition congrS_dec {n} {x} {y} (H :congr n x y) : congrS n x y.

End Congruence.

Hint Resolve congr_refl congr_trans congr_sym congr_0_eq congr_1 : congr.

Notation "x ≡ y [ n ]" := (congr n x y) (at level 80).

Section ggT.

Variables a b : Z.
Hypothesis a_pos : 0 a.
Hypothesis b_pos : 0 b.

Inductive Eucl : Set :=
| Eucl_intro : (u v d:Z) (Hbez:u × a + v × b = d)
(Hpos: 0 d)
(Hgcd: Zis_gcd a b d), Eucl.

The recursive part of Euclid's algorithm uses well-founded recursion of non-negative integers. It maintains 6 integers u1,u2,u3,v1,v2,v3 such that the following invariant holds: u1×a+u2×b=u3 and v1×a+v2×b=v3 and gcd(u2,v3)=gcd(a,b).

Lemma eucl_rec :
(v3:Z) (Hv3: 0 v3)
(u3 : Z),
0 u3
u1 u2 v1 v2:Z,
u1 × a + u2 × b = u3
v1 × a + v2 × b = v3
( d:Z, Zis_gcd u3 v3 dZis_gcd a b d) → Eucl.

We get Euclid's algorithm by applying euclid_rec on 1,0,a,0,1,b when b>=0 and 1,0,a,0,-1,-b when b<0.

Lemma eucl : Eucl.

Definition ggT := match eucl with
Eucl_intro _ _ g _ _ _g
end.

Lemma ggT_pos : 0 ggT.

Lemma ggT_is_Zgcd : ggT = Zgcd a b.

End ggT.

Section on_gcd.

Variables a b : Z.

Lemma Zgcd_divides_l : (Zgcd a b | a).

Lemma Zgcd_divides_r : (Zgcd a b | b).

Lemma Zis_gcd_0_inv_l : Zis_gcd a b 0 → a = 0.

Lemma Zis_gcd_0_inv_r : Zis_gcd a b 0 → b = 0.

End on_gcd.

Section RemEqn.

Variables a b ma mb : Z.
Hypothesis Hma : 0 ma.
Hypothesis Hmb : 0 mb.

Definition rem_eqn_spec n := congr ma a n congr mb b n.

Lemma rem_eqn_nes n : rem_eqn_spec n
congr (Zgcd ma mb) a b.

Definition rem_eqn_particular : congr (Zgcd ma mb) a b
{ n : Z | rem_eqn_spec n}.

Lemma rem_eqn_other_solution' :
(H : congr (Zgcd ma mb) a b),
let (n, _) := rem_eqn_particular H in
k, rem_eqn_spec (n + k × Z.lcm ma mb).

Lemma rem_eqn_other_solution :
{n} k, rem_eqn_spec (n + k × Z.lcm ma mb) →
rem_eqn_spec n.

Lemma rem_eqn_other_solution_congr :
{n m}, n m [Z.lcm ma mb]
rem_eqn_spec m
rem_eqn_spec n.

Lemma rem_eqn_all_solutions' :
N (Hsol: rem_eqn_spec N),
let H := rem_eqn_nes N Hsol in
let (n, _) := rem_eqn_particular H in
N n [Z.lcm ma mb].

Lemma rem_eqn_all_solutions :
N n, rem_eqn_spec Nrem_eqn_spec n
N n [Z.lcm ma mb].

Lemma rem_eqn_0_l : {n},
ma = 0 → rem_eqn_spec nn = a.

Definition smallest_larger_than (m: Z) (P : ZProp) (n: Z) : Prop :=
P n m n q, P qm qn q.

Lemma smallest_larger_than_unique m P n n' :
smallest_larger_than m P n
smallest_larger_than m P n'
n = n'.

Definition largest_smaller_than (m: Z) (P : ZProp) (n: Z) : Prop :=
P n n m q, P qq mq n.

Lemma largest_smaller_than_unique m P n n' :
largest_smaller_than m P n
largest_smaller_than m P n'
n = n'.

Lemma smallest_solution_larger_than' A :
Z.lcm ma mb > 0 →
q n,
rem_eqn_spec q
rem_eqn_spec (A + (n - A) mod Z.lcm ma mb) →
A q
A + (n - A) mod Z.lcm ma mb q.

Lemma smallest_solution_larger_than H A :
Z.lcm ma mb > 0 →
smallest_larger_than A rem_eqn_spec (A + (proj1_sig (rem_eqn_particular H) - A) mod Z.lcm ma mb).

Lemma largest_solution_smaller_than H B :
Z.lcm ma mb > 0 →
largest_smaller_than B rem_eqn_spec (B - (B - proj1_sig (rem_eqn_particular H)) mod Z.lcm ma mb).

End RemEqn.

Require Import Utf8.
Require Psatz.

Lemma le_congr i j s :
i < j
i j [Zpos s]
i j - Zpos s.

Definition Nabs_diff (x y: Z) := N_of_Z (Zmax (x - y) (y - x)).
Lemma Nabs_diff_case x y :
x y Nabs_diff x y = N_of_Z (y - x)
y x Nabs_diff x y = N_of_Z (x - y).

Definition Zdivides_dec (a b: Z) : { (a | b) } + { ¬ (a | b) }.

Local Coercion Z_of_N : N >-> Z.
Definition Ndivides_dec (a b: N) : { (a | b) } + { ¬ (a | b) }.

Remark Ngcd_is_Zgcd (x y: N) : (N.gcd x y:Z) = Zgcd x y.

Remark Nlcm_is_Zlcm (x y: N) : (N.lcm x y:Z) = Z.lcm x y.

Lemma N_of_pos (x: Z) : 0 x (N_of_Z x : Z) = x.