Require Import ZArith.
Require Import ZArithRing.
Require Import Zcomplements.

Inductive divide (a b : Z) : Prop :=
    divide_intro : ∀ q : Z, b = (q × a)%Z → divide a b.

Notation "( x | y )" := (divide x y) (at level 0) : Z_scope.

Open Local Scope Z_scope.

Lemma divide_refl : ∀ a : Z, (a | a).
Proof.
intros; apply divide_intro with 1; ring.
Qed.

Lemma one_divide : ∀ a : Z, (1 | a).
Proof.
intros; apply divide_intro with a; ring.
Qed.

Lemma divide_0 : ∀ a : Z, (a | 0).
Proof.
intros; apply divide_intro with 0; ring.
Qed.

Hint Resolve divide_refl one_divide divide_0.

Lemma divide_mult_left : ∀ a b c : Z, (a | b) → (c × a | c × b).
Proof.
simple induction 1; intros; apply divide_intro with q.
rewrite H0; ring.
Qed.

Lemma divide_mult_right : ∀ a b c : Z, (a | b) → (a × c | b × c).
Proof.
intros a b c; rewrite (Zmult_comm a c); rewrite (Zmult_comm b c).
apply divide_mult_left; trivial.
Qed.

Hint Resolve divide_mult_left divide_mult_right.

Lemma divide_plus : ∀ a b c : Z, (a | b) → (a | c) → (a | b + c).
Proof.
simple induction 1; intros q Hq; simple induction 1; intros q' Hq'.
apply divide_intro with (q + q').
rewrite Hq; rewrite Hq'; ring.
Qed.

Lemma divide_opp : ∀ a b : Z, (a | b) → (a | - b).
Proof.
simple induction 1; intros; apply divide_intro with (- q).
rewrite H0; ring.
Qed.

Lemma divide_opp_rev : ∀ a b : Z, (a | - b) → (a | b).
Proof.
intros; replace b with (- - b). apply divide_opp; trivial. ring.
Qed.

Lemma divide_opp_left : ∀ a b : Z, (a | b) → (- a | b).
Proof.
simple induction 1; intros; apply divide_intro with (- q).
rewrite H0; ring.
Qed.

Lemma divide_opp_left_rev : ∀ a b : Z, (- a | b) → (a | b).
Proof.
intros; replace a with (- - a). apply divide_opp_left; trivial. ring.
Qed.

Lemma divide_minus : ∀ a b c : Z, (a | b) → (a | c) → (a | b - c).
Proof.
simple induction 1; intros q Hq; simple induction 1; intros q' Hq'.
apply divide_intro with (q - q').
rewrite Hq; rewrite Hq'; ring.
Qed.

Lemma divide_left : ∀ a b c : Z, (a | b) → (a | b × c).
Proof.
simple induction 1; intros q Hq; apply divide_intro with (q × c).
rewrite Hq; ring.
Qed.

Lemma divide_right : ∀ a b c : Z, (a | c) → (a | b × c).
Proof.
simple induction 1; intros q Hq; apply divide_intro with (q × b).
rewrite Hq; ring.
Qed.

Lemma divide_a_ab : ∀ a b : Z, (a | a × b).
Proof.
intros; apply divide_intro with b; ring.
Qed.

Lemma divide_a_ba : ∀ a b : Z, (a | b × a).
Proof.
intros; apply divide_intro with b; ring.
Qed.

Hint Resolve divide_plus divide_opp divide_opp_rev divide_opp_left
  divide_opp_left_rev divide_minus divide_left divide_right divide_a_ab
  divide_a_ba.

Lemma z_case_0_1 :
 ∀ x : Z, x ≤ -2 ∨ x = -1 ∨ x = 0 ∨ x = 1 ∨ x ≥ 2.
Proof. intro; omega. Qed.

Lemma z_case_0 : ∀ x : Z, x ≤ -1 ∨ x = 0 ∨ x ≥ 1.
Proof. intro; omega. Qed.

Lemma divide_1 : ∀ x : Z, (x | 1) → x = 1 ∨ x = -1.
Proof.
simple induction 1; intros.
elim (z_case_0_1 x); intuition; elim (z_case_0 q); intuition.
assert (q × x ≥ 1 × 2).
replace (q × x) with (- q × - x); try ring.
apply Zmult_ge_compat; omega.
omega.
rewrite H3 in H0; omega.
assert (- (q × x) ≥ 1 × 2).
replace (- (q × x)) with (q × - x); try ring.
apply Zmult_ge_compat; omega.
omega.
rewrite H1 in H0; omega.
rewrite H1 in H0; omega.
rewrite H1 in H0; omega.
assert (- (q × x) ≥ 1 × 2).
replace (- (q × x)) with (- q × x); try ring.
apply Zmult_ge_compat; omega.
omega.
rewrite H3 in H0; omega.
assert (q × x ≥ 1 × 2).
apply Zmult_ge_compat; omega.
omega.
Qed.

Lemma divide_antisym : ∀ a b : Z, (a | b) → (b | a) → a = b ∨ a = - b.
Proof.
simple induction 1; intros.
inversion H1.
rewrite H0 in H2; clear H H1.
case (Z_zerop a); intro.
left; rewrite H0; rewrite e; ring.
assert (Hqq0 : q0 × q = 1).
apply Zmult_reg_l with a.
assumption.
ring_simplify.
pattern a at 2 in |- *; rewrite H2; ring.
assert (q | 1).
rewrite <- Hqq0; auto.
elim (divide_1 q H); intros.
rewrite H1 in H0; left; omega.
rewrite H1 in H0; right; omega.
Qed.

Lemma Zabs_ind :
 ∀ (P : Z → Prop) (x : Z),
 (x ≥ 0 → P x) → (x ≤ 0 → P (- x)) → P (Zabs x).
Proof.
intros; elim (Z_lt_ge_dec x 0); intro.
rewrite Zabs_non_eq. apply H0; omega. omega.
rewrite Zabs_eq. apply H; assumption. omega.
Qed.

Lemma divide_bounds : ∀ a b : Z, (a | b) → b ≠ 0 → Zabs a ≤ Zabs b.
Proof.
simple induction 1; intros.
pattern (Zabs a) in |- *; apply Zabs_ind; pattern (Zabs b) in |- *;
 apply Zabs_ind; intros.
elim (z_case_0 q); intro.
assert (- b ≥ 1 × 0).
replace (- b) with (- q × a).
apply Zmult_ge_compat; omega.
rewrite H0; ring. omega.
elim H4; intro; clear H4.
rewrite H5 in H0; omega.
apply Zge_le.
replace a with (1 × a).
rewrite H0.
apply Zmult_ge_compat; omega.
ring.
elim (z_case_0 q); intro.
apply Zge_le.
replace a with (1 × a).
rewrite H0.
replace (- (q × a)) with (- q × a).
apply Zmult_ge_compat; omega.
ring. ring.
elim H4; intro; clear H4.
rewrite H5 in H0; omega.
assert (b ≥ 1 × 0).
rewrite H0.
apply Zmult_ge_compat; omega.
omega.
elim (z_case_0 q); intro.
apply Zge_le.
replace (- a) with (1 × - a).
rewrite H0.
replace (q × a) with (- q × - a).
apply Zmult_ge_compat; omega.
ring. ring.
elim H4; intro; clear H4.
rewrite H5 in H0; omega.
assert (- b ≥ 1 × 0).
rewrite H0.
replace (- (q × a)) with (q × - a).
apply Zmult_ge_compat; omega.
ring. omega.
elim (z_case_0 q); intro.
assert (b ≥ 1 × 0).
rewrite H0.
replace (q × a) with (- q × - a).
apply Zmult_ge_compat; omega.
ring. omega.
elim H4; intro; clear H4.
rewrite H5 in H0; omega.
apply Zge_le.
replace (- a) with (1 × - a).
rewrite H0.
replace (- (q × a)) with (q × - a).
apply Zmult_ge_compat; omega.
ring. ring.
Qed.