Require Import ZArith.

Require Import lemmas.
Require Import natZ.
Require Import exp.
Require Import divides.

Definition Mod (a b : Z) (n : nat) :=
  ∃ q : Z, a = (b + Z_of_nat n × q)%Z.

Lemma modpq_modp : ∀ (a b : Z) (p q : nat), Mod a b (p × q) → Mod a b p.
Proof.
   unfold Mod in |- ×.
   intros.
   elim H.
   intros.
   split with (Z_of_nat q × x)%Z.
   rewrite (Znat.inj_mult p q) in H0.
   rewrite Zmult_assoc.
   assumption.
Qed.

Lemma mod_refl : ∀ (a : Z) (n : nat), Mod a a n.
Proof.
   unfold Mod in |- ×. intros.
   split with 0%Z.
   rewrite <- Zmult_0_r_reverse.
   rewrite <- Zplus_0_r_reverse.
   reflexivity.
Qed.

Lemma mod_sym : ∀ (a b : Z) (n : nat), Mod a b n → Mod b a n.
Proof.
   unfold Mod in |- ×. intros.
   elim H.
   intros.
   split with (- x)%Z.
   simpl in |- ×.
   rewrite H0.
   simpl in |- ×.
   rewrite Zplus_assoc_reverse.
   rewrite <- Zmult_plus_distr_r.
   rewrite Zplus_opp_r.
   rewrite <- Zmult_0_r_reverse.
   apply Zplus_0_r_reverse.
Qed.

Lemma mod_trans :
 ∀ (a b c : Z) (n : nat), Mod a b n → Mod b c n → Mod a c n.
Proof.
   unfold Mod in |- ×. intros.
   elim H. elim H0.
   intros. rewrite H2. rewrite H1.
   split with (x + x0)%Z.
   rewrite Zmult_plus_distr_r.
   rewrite (Zplus_assoc c (Z_of_nat n × x) (Z_of_nat n × x0)).
   reflexivity.
Qed.

Lemma eqmod : ∀ x y : Z, x = y → ∀ n : nat, Mod x y n.
Proof.
   intros. rewrite H. apply mod_refl.
Qed.

Lemma mod_plus_compat :
 ∀ (a b c d : Z) (n : nat),
 Mod a b n → Mod c d n → Mod (a + c) (b + d) n.
Proof.
   unfold Mod in |- ×. intros.
   elim H. elim H0.
   intros. split with (x + x0)%Z.
   rewrite H1.
   rewrite H2.
   rewrite (Zplus_assoc (b + Z_of_nat n × x0) d (Z_of_nat n × x)).
   rewrite (Zplus_assoc_reverse b (Z_of_nat n × x0) d).
   rewrite (Zplus_comm (Z_of_nat n × x0) d).
   rewrite (Zplus_comm x x0).
   rewrite (Zmult_plus_distr_r (Z_of_nat n) x0 x).
   rewrite Zplus_assoc.
   rewrite Zplus_assoc.
   reflexivity.
Qed.

Lemma mod_mult_compat :
 ∀ (a b c d : Z) (n : nat),
 Mod a b n → Mod c d n → Mod (a × c) (b × d) n.
Proof.
   unfold Mod in |- ×. intros.
   elim H. elim H0.
   intros. rewrite H1. rewrite H2. split with (x0 × d + x × b + Z_of_nat n × x0 × x)%Z.
   rewrite (Zmult_plus_distr_r (b + Z_of_nat n × x0) d (Z_of_nat n × x)).
   rewrite Zmult_plus_distr_l.
   rewrite Zmult_plus_distr_l.
   rewrite (Zmult_assoc b (Z_of_nat n) x).
   rewrite (Zmult_comm b (Z_of_nat n)).
   rewrite (Zmult_assoc (Z_of_nat n × x0) (Z_of_nat n) x).
   rewrite (Zmult_assoc_reverse (Z_of_nat n) x0 (Z_of_nat n)).
   rewrite (Zmult_assoc_reverse (Z_of_nat n) (x0 × Z_of_nat n) x).
   rewrite (Zmult_assoc_reverse (Z_of_nat n) b x).
   rewrite <- (Zmult_plus_distr_r (Z_of_nat n) (b × x) (x0 × Z_of_nat n × x)).
   rewrite (Zplus_assoc_reverse (b × d)).
   rewrite (Zmult_assoc_reverse (Z_of_nat n) x0 d).
   rewrite <-
    (Zmult_plus_distr_r (Z_of_nat n) (x0 × d) (b × x + x0 × Z_of_nat n × x))
    .
   rewrite (Zmult_comm x0 (Z_of_nat n)).
   rewrite Zplus_assoc.
   rewrite (Zmult_comm b x).
   reflexivity.
Qed.

Lemma mod_sqr_compat :
 ∀ (a b : Z) (n : nat), Mod a b n → Mod (a × a) (b × b) n.
Proof.
   intros. apply mod_mult_compat. assumption. assumption.
Qed.

Lemma mod_exp_compat :
 ∀ (a b : Z) (n : nat),
 Mod a b n → ∀ m : nat, Mod (Exp a m) (Exp b m) n.
Proof.
   simple induction m.
   simpl in |- ×. apply mod_refl.
   intros m1 IHm. simpl in |- ×.
   apply mod_mult_compat.
   assumption. assumption.
Qed.

Lemma moda0_exp_compat :
 ∀ (a : Z) (n : nat),
 n > 0 → Mod a 0 n → ∀ m : nat, m > 0 → Mod (Exp a m) 0 n.
Proof.
   intros a n.
   case n.
   intro.
   elim (lt_irrefl 0).
   assumption.
   intro.
   intro.
   intro.
   intro.
   case m.
   intro.
   elim (lt_irrefl 0).
   assumption.
   intro m0.
   intros.
   elim H0.
   intros.
   rewrite H2.
   split with (x × Exp (Z_of_nat (S n0) × x) m0)%Z.
   rewrite Zmult_assoc.
   simpl in |- ×.
   reflexivity.
Qed.

Lemma mod_opp_compat :
 ∀ (a b : Z) (n : nat), Mod a b n → Mod (- a) (- b) n.
Proof.
   intros. elim H. intros.
   split with (- x)%Z. rewrite H0.
   rewrite Zopp_eq_mult_neg_1.
   rewrite Zopp_eq_mult_neg_1.
   rewrite Zopp_eq_mult_neg_1.
   rewrite Zmult_assoc.
   rewrite <- Zmult_plus_distr_l.
   reflexivity.
Qed.

Lemma mod_minus_compat :
 ∀ (a b c d : Z) (n : nat),
 Mod a b n → Mod c d n → Mod (a - c) (b - d) n.
Proof.
   intros.
   unfold Zminus in |- ×.
   apply mod_plus_compat.
   assumption.
   apply mod_opp_compat.
   assumption.
Qed.

Lemma mod_nx_0_n : ∀ (n : nat) (x : Z), Mod (Z_of_nat n × x) 0 n.
Proof.
   intros. unfold Mod in |- ×.
   split with x.
   simpl in |- ×. reflexivity.
Qed.

Lemma moddivmin :
 ∀ (a b : Z) (n : nat), Mod a b n ↔ Divides n (Zabs_nat (a - b)).
Proof.
   unfold Mod, Divides in |- ×. split.
   intros.
   elim H.
   intros.
   rewrite H0.
   unfold Zminus in |- ×.
   rewrite Zplus_assoc_reverse.
   rewrite Zplus_comm.
   rewrite Zplus_assoc_reverse.
   rewrite (Zplus_comm (- b) b).
   rewrite Zplus_opp_r.
   rewrite <- Zplus_0_r_reverse.
   split with (Zabs_nat x).
   pattern n at 2 in |- ×.
   rewrite <- (abs_inj n).
   apply abs_mult.
   intros. elim H. intros.
   elim (Zle_or_lt b a).
   split with (Z_of_nat x).
   rewrite <- Znat.inj_mult.
   rewrite <- H0.
   rewrite inj_abs_pos.
   unfold Zminus in |- ×.
   rewrite Zplus_assoc.
   rewrite Zplus_comm.
   rewrite Zplus_assoc.
   rewrite Zplus_opp_l.
   simpl in |- ×. reflexivity.
   apply Zle_ge.
   replace 0%Z with (b - b)%Z. unfold Zminus in |- ×.
   apply Zplus_le_compat_r. assumption.
   unfold Zminus in |- ×.
   apply Zplus_opp_r.
   split with (- Z_of_nat x)%Z.
   rewrite Zmult_comm.
   rewrite Zopp_mult_distr_l_reverse.
   rewrite <- Znat.inj_mult.
   rewrite mult_comm.
   rewrite <- H0.
   rewrite inj_abs_neg.
   rewrite Zopp_involutive.
   unfold Zminus in |- ×.
   rewrite (Zplus_comm a).
   rewrite Zplus_assoc.
   rewrite Zplus_opp_r.
   simpl in |- ×. reflexivity.
   replace 0%Z with (b - b)%Z. unfold Zminus in |- ×.
   rewrite (Zplus_comm a). rewrite (Zplus_comm b). apply Zplus_lt_compat_l.
   assumption.
   unfold Zminus in |- ×. apply Zplus_opp_r.
Qed.

Lemma moddec : ∀ (a b : Z) (n : nat), Mod a b n ∨ ¬ Mod a b n.
Proof.
   intros.
   elim (moddivmin a b n). intros.
   elim (divdec (Zabs_nat (a - b)) n).
   left. apply H0. assumption.
   right. intro. elim H1. apply H. assumption.
Qed.

Lemma mod_0not1 : ∀ n : nat, n > 1 → ¬ Mod 0 1 n.
Proof.
   intros.
   intro.
   absurd (Divides n 1).
   intro.
   elim (le_not_lt n 1).
   apply div_le1.
   assumption.
   assumption.
   elim (moddivmin 0 1 n).
   intros.
   apply H1.
   assumption.
Qed.

Lemma mod_exp1 :
 ∀ (a : Z) (n : nat), Mod a 1 n → ∀ m : nat, Mod (Exp a m) 1 n.
Proof.
   intros a n H.
   simple induction m.
   simpl in |- ×.
   apply mod_refl.
   intros m1 IH.
   simpl in |- ×.
   replace 1%Z with (1 × 1)%Z.
   apply mod_mult_compat.
   assumption.
   apply IH.
   simpl in |- ×.
   reflexivity.
Qed.

Lemma mod_repr_non_0 :
 ∀ (n : nat) (x : Z), (0 < x < Z_of_nat n)%Z → ¬ Mod x 0 n.
Proof.
   intros.
   intro.
   elim H.
   intros.
   elim (moddivmin x 0 n).
   rewrite <- Zminus_0_l_reverse.
   intros.
   elim (le_not_lt n (Zabs_nat x)).
   apply div_le.
   change (Zabs_nat 0 < Zabs_nat x) in |- ×.
   apply ltzlt.
   unfold Zle in |- ×.
   simpl in |- ×.
   discriminate.
   apply Zlt_le_weak.
   assumption.
   assumption.
   apply H3.
   assumption.
   rewrite <- (abs_inj n).
   apply ltzlt.
   apply Zlt_le_weak.
   assumption.
   change (Z_of_nat 0 ≤ Z_of_nat n)%Z in |- ×.
   apply Znat.inj_le.
   apply le_O_n.
   assumption.
Qed.

Lemma mod_repr_eq :
 ∀ (p : nat) (x y : Z),
 0 < p →
 (0 < x < Z_of_nat p)%Z → (0 < y < Z_of_nat p)%Z → Mod x y p → x = y.
Proof.
   intros. unfold Mod in H2.
   elim H2. intros q Hq.
   rewrite Hq in H0.
   elim H0. elim H1. intros.
   elim (Zle_or_lt 0 q).
   intro. elim (Zle_lt_or_eq 0 q).

   intro. elim (Zlt_not_le 0 y).
   assumption. apply Zplus_le_reg_l with (Z_of_nat p).
   rewrite (Zplus_comm (Z_of_nat p)).
   rewrite (Zplus_comm (Z_of_nat p)). simpl in |- ×.
   apply Zlt_le_weak.
   apply Zle_lt_trans with (y + Z_of_nat p × q)%Z.
   apply Zplus_le_compat_l. pattern (Z_of_nat p) at 1 in |- ×.
   rewrite <- Zmult_1_l with (Z_of_nat p).
   rewrite (Zmult_comm 1). apply Zle_mult_l.
   change (Z_of_nat 0 < Z_of_nat p)%Z in |- ×.
   apply Znat.inj_lt. assumption.
   change (Zsucc 0 ≤ q)%Z in |- ×. apply Zlt_le_succ. assumption.
   assumption.

   intro. rewrite <- H8 in Hq. rewrite Zmult_comm in Hq.
   rewrite Zplus_comm in Hq. simpl in Hq. assumption.

   assumption.

   intro. elim (Zlt_not_le 0 (y + Z_of_nat p × q)).
   assumption. apply Zle_trans with (y + Z_of_nat p × -1)%Z.
   apply Zplus_le_compat_l. apply Zle_mult_l.
   change (Z_of_nat 0 < Z_of_nat p)%Z in |- ×. apply Znat.inj_lt.
   assumption. apply Zlt_succ_le. simpl in |- ×. assumption.
   apply Zplus_le_reg_l with (Z_of_nat p).
   rewrite (Zplus_comm (Z_of_nat p)).
   rewrite (Zplus_comm (Z_of_nat p)).
   rewrite (Zmult_comm (Z_of_nat p)).
   rewrite (Zopp_mult_distr_l_reverse 1). rewrite Zmult_1_l.
   rewrite Zplus_assoc_reverse. rewrite Zplus_opp_l.
   rewrite (Zplus_comm y 0). simpl in |- ×. apply Zlt_le_weak.
   assumption.
Qed.

Definition ZMod (a b n : Z) := ∃ q : Z, a = (b + n × q)%Z.

Lemma zmodpq_modp : ∀ a b p q : Z, ZMod a b (p × q) → ZMod a b p.
Proof.
   unfold ZMod in |- ×.
   intros.
   elim H.
   intros.
   split with (q × x)%Z.
   rewrite Zmult_assoc.
   assumption.
Qed.

Lemma zmod_refl : ∀ a n : Z, ZMod a a n.
Proof.
   unfold ZMod in |- ×. intros.
   split with 0%Z.
   rewrite <- Zmult_0_r_reverse.
   rewrite <- Zplus_0_r_reverse.
   reflexivity.
Qed.

Lemma zmod_sym : ∀ a b n : Z, ZMod a b n → ZMod b a n.
Proof.
   unfold ZMod in |- ×. intros.
   elim H.
   intros.
   split with (- x)%Z.
   simpl in |- ×.
   rewrite H0.
   simpl in |- ×.
   rewrite Zplus_assoc_reverse.
   rewrite <- Zmult_plus_distr_r.
   rewrite Zplus_opp_r.
   rewrite <- Zmult_0_r_reverse.
   apply Zplus_0_r_reverse.
Qed.

Lemma zmod_trans : ∀ a b c n : Z, ZMod a b n → ZMod b c n → ZMod a c n.
Proof.
   unfold ZMod in |- ×. intros.
   elim H. elim H0.
   intros. rewrite H2. rewrite H1.
   split with (x + x0)%Z.
   rewrite Zmult_plus_distr_r.
   rewrite (Zplus_assoc c (n × x) (n × x0)).
   reflexivity.
Qed.

Lemma zeqmod : ∀ x y : Z, x = y → ∀ n : Z, ZMod x y n.
Proof.
   intros. rewrite H. apply zmod_refl.
Qed.

Lemma zmod_plus_compat :
 ∀ a b c d n : Z, ZMod a b n → ZMod c d n → ZMod (a + c) (b + d) n.
Proof.
   unfold ZMod in |- ×. intros.
   elim H. elim H0.
   intros. split with (x + x0)%Z.
   rewrite H1.
   rewrite H2.
   rewrite (Zplus_assoc (b + n × x0) d (n × x)).
   rewrite (Zplus_assoc_reverse b (n × x0) d).
   rewrite (Zplus_comm (n × x0) d).
   rewrite (Zplus_comm x x0).
   rewrite (Zmult_plus_distr_r n x0 x).
   rewrite Zplus_assoc.
   rewrite Zplus_assoc.
   reflexivity.
Qed.

Lemma zmod_mult_compat :
 ∀ a b c d n : Z, ZMod a b n → ZMod c d n → ZMod (a × c) (b × d) n.
Proof.
   unfold ZMod in |- ×. intros.
   elim H. elim H0.
   intros. rewrite H1. rewrite H2. split with (x0 × d + x × b + n × x0 × x)%Z.
   rewrite (Zmult_plus_distr_r (b + n × x0) d (n × x)).
   rewrite Zmult_plus_distr_l.
   rewrite Zmult_plus_distr_l.
   rewrite (Zmult_assoc b n x).
   rewrite (Zmult_comm b n).
   rewrite (Zmult_assoc (n × x0) n x).
   rewrite (Zmult_assoc_reverse n x0 n).
   rewrite (Zmult_assoc_reverse n (x0 × n) x).
   rewrite (Zmult_assoc_reverse n b x).
   rewrite <- (Zmult_plus_distr_r n (b × x) (x0 × n × x)).
   rewrite (Zplus_assoc_reverse (b × d)).
   rewrite (Zmult_assoc_reverse n x0 d).
   rewrite <- (Zmult_plus_distr_r n (x0 × d) (b × x + x0 × n × x)).
   rewrite (Zmult_comm x0 n).
   rewrite Zplus_assoc.
   rewrite (Zmult_comm b x).
   reflexivity.
Qed.

Lemma zmod_sqr_compat :
 ∀ a b n : Z, ZMod a b n → ZMod (a × a) (b × b) n.
Proof.
   intros. apply zmod_mult_compat. assumption. assumption.
Qed.

Lemma zmodmod : ∀ a b n : Z, ZMod a b n → Mod a b (Zabs_nat n).
Proof.
   unfold ZMod, Mod in |- ×.
   intros. elim H. intros.
   rewrite H0.
   elim (Zle_or_lt 0 n).
   intro. rewrite inj_abs_pos.
   split with x. reflexivity.
   apply Zle_ge. assumption.
   intro. rewrite inj_abs_neg.
   split with (- x)%Z. rewrite Zopp_mult_distr_l_reverse.
   rewrite Zopp_mult_distr_r. rewrite Zopp_involutive.
   reflexivity.
   assumption.
Qed.

Lemma modzmod :
 ∀ (a b : Z) (n : nat), Mod a b n → ZMod a b (Z_of_nat n).
Proof.
   unfold Mod, ZMod in |- ×. intros. elim H.
   intros. rewrite H0. split with x.
   reflexivity.
Qed.

Lemma absmodzmod : ∀ a b n : Z, Mod a b (Zabs_nat n) → ZMod a b n.
Proof.
   intros.
   elim H. intros q Hq.
   elim Zle_or_lt with 0%Z n.
   intro. split with q. rewrite inj_abs_pos in Hq.
   assumption. apply Zle_ge. assumption.
   intros. split with (- q)%Z. rewrite inj_abs_neg in Hq.
   rewrite Zmult_comm. rewrite Zopp_mult_distr_l_reverse.
   rewrite Zopp_mult_distr_l_reverse in Hq. rewrite Zmult_comm.
   assumption. assumption.
Qed.

Lemma zmod_exp_compat :
 ∀ a b n : Z, ZMod a b n → ∀ m : Z, ZMod (ZExp a m) (ZExp b m) n.
Proof.
   intros.
   apply absmodzmod.
   rewrite expzexp.
   rewrite expzexp.
   apply mod_exp_compat.
   apply zmodmod.
   assumption.
Qed.

Lemma zmoda0_exp_compat :
 ∀ a n : Z,
 (n > 0)%Z → ZMod a 0 n → ∀ m : Z, (m > 0)%Z → ZMod (ZExp a m) 0 n.
Proof.
   intros. rewrite <- (inj_abs_pos n).
   apply modzmod. rewrite expzexp.
   apply moda0_exp_compat.
   change (Zabs_nat n > Zabs_nat 0) in |- ×. apply gtzgt.
   apply Zlt_le_weak. apply Zgt_lt. assumption.
   apply Zeq_le. reflexivity.
   assumption.
   apply zmodmod. assumption.
   change (Zabs_nat m > Zabs_nat 0) in |- ×. apply gtzgt.
   apply Zlt_le_weak. apply Zgt_lt. assumption.
   apply Zeq_le. reflexivity.
   assumption.
   apply Zle_ge. apply Zlt_le_weak. apply Zgt_lt. assumption.
Qed.

Lemma zmod_opp_compat : ∀ a b n : Z, ZMod a b n → ZMod (- a) (- b) n.
Proof.
   intros. elim H. intros.
   split with (- x)%Z. rewrite H0.
   rewrite Zopp_eq_mult_neg_1.
   rewrite Zopp_eq_mult_neg_1.
   rewrite Zopp_eq_mult_neg_1.
   rewrite Zmult_assoc.
   rewrite <- Zmult_plus_distr_l.
   reflexivity.
Qed.

Lemma zmod_minus_compat :
 ∀ a b c d n : Z, ZMod a b n → ZMod c d n → ZMod (a - c) (b - d) n.
Proof.
   intros.
   unfold Zminus in |- ×.
   apply zmod_plus_compat.
   assumption.
   apply zmod_opp_compat.
   assumption.
Qed.

Lemma zmod_nx_0_n : ∀ n x : Z, ZMod (n × x) 0 n.
Proof.
   intros. unfold ZMod in |- ×.
   split with x.
   simpl in |- ×. reflexivity.
Qed.

Lemma zmoddivmin : ∀ a b n : Z, ZMod a b n ↔ ZDivides n (a - b).
Proof.
   unfold ZMod, Divides in |- ×. split.

   intros. elim H. intros.
   rewrite H0.
   unfold Zminus in |- ×.
   rewrite Zplus_assoc_reverse.
   rewrite Zplus_comm.
   rewrite Zplus_assoc_reverse.
   rewrite (Zplus_comm (- b) b).
   rewrite Zplus_opp_r.
   rewrite <- Zplus_0_r_reverse.
   split with x.
   reflexivity.

   intros. elim H. intros.
   split with x.
   rewrite <- H0.
   unfold Zminus in |- ×.
   rewrite Zplus_assoc.
   rewrite Zplus_comm.
   rewrite Zplus_assoc.
   rewrite Zplus_opp_l.
   simpl in |- ×. reflexivity.
Qed.

Lemma zmoddec : ∀ a b n : Z, ZMod a b n ∨ ¬ ZMod a b n.
Proof.
   intros.
   elim (zmoddivmin a b n).
   intros.
   elim (zdivdec (a - b) n).
   left.
   apply H0.
   assumption.
   right.
   intro.
   elim H1.
   apply H.
   assumption.
Qed.

Lemma zmod_0not1 : ∀ n : Z, (n > 1)%Z → ¬ ZMod 0 1 n.
Proof.
   intros. intro.
   elim (mod_0not1 (Zabs_nat n)).
   change (Zabs_nat n > Zabs_nat 1) in |- ×. apply gtzgt.
   apply Zlt_le_weak. apply Zlt_trans with 1%Z.
   unfold Zlt in |- ×. simpl in |- ×. reflexivity.
   apply Zgt_lt. assumption.
   unfold Zle in |- ×. simpl in |- ×. discriminate.
   assumption.
   apply zmodmod. assumption.
Qed.

Lemma zmod_repr_non_0 : ∀ n x : Z, (0 < x < n)%Z → ¬ ZMod x 0 n.
Proof.
   intros.
   intro.
   elim H.
   intros.
   elim (mod_repr_non_0 (Zabs_nat n) x).
   split.
   assumption. rewrite inj_abs_pos.
   assumption. apply Zle_ge. apply Zle_trans with x.
   apply Zlt_le_weak. assumption.
   apply Zlt_le_weak. assumption.
   apply zmodmod. assumption.
Qed.