Require Export ZGcd.

Section zmod.

Definition Zmod_same := Z_mod_same.

Lemma Zmod_zero_lft : ∀ m : Z, (0 mod m)%Z = 0%Z.
Proof.
 intro m.
 case m; auto.
Qed.

Lemma Zmod_zero_rht : ∀ a : Z, (a mod 0)%Z = 0%Z.
Proof.
 intro a.
 case a; auto.
Qed.

Lemma Zmod_Zmod :
 ∀ m a : Z, (m > 0)%Z → ((a mod m) mod m)%Z = (a mod m)%Z.
Proof.
 intros m a Hm.
 apply (Zdiv_remainder_unique (a mod m) m (a mod m / m) ((a mod m) mod m) 0 (a mod m)).
    rewrite Zmult_comm.
    apply Z_div_mod_eq; auto.
   apply Z_mod_lt; auto.
  auto with zarith.
 apply Z_mod_lt; auto.
Qed.

Lemma Zmod_cancel_multiple :
 ∀ m a b : Z, (m > 0)%Z → ((b × m + a) mod m)%Z = (a mod m)%Z.
Proof.
 intros m a b Hm.
 rewrite Zplus_comm.
 apply Z_mod_plus.
 exact Hm.
Qed.

Lemma Zmod_multiple : ∀ m a : Z, (m > 0)%Z → ((a × m) mod m)%Z = 0%Z.
Proof.
 intros m a Hm.
 rewrite <- (Zplus_0_r (a × m)).
 rewrite Zmod_cancel_multiple; auto.
Qed.

Lemma Zmod_minus_intro :
 ∀ m a b : Z,
 (m > 0)%Z → ((a - b) mod m)%Z = 0%Z → (a mod m)%Z = (b mod m)%Z.
Proof.
 intros m a b Hm H0.
 assert (Hdiv : Zdivides m (a - b)); auto with zarith.
 elim Hdiv; intros q Hq.
 replace a with (q × m + b)%Z; auto with zarith.
 apply Zmod_cancel_multiple.
 assumption.
Qed.

Lemma Zmod_plus_compat :
 ∀ m a b : Z,
 (m > 0)%Z → ((a + b) mod m)%Z = ((a mod m + b mod m) mod m)%Z.
Proof.
 intros m a b Hm.
 rewrite <- (Zmod_Zmod m (a + b) Hm).
 apply Zmod_minus_intro.
  exact Hm.
 apply Zmod0_Zdivides.
  auto with zarith.
 replace (a mod m)%Z with (a - m × (a / m))%Z.
  replace (b mod m)%Z with (b - m × (b / m))%Z.
   replace ((a + b) mod m)%Z with (a + b - m × ((a + b) / m))%Z.
    unfold Zminus in |- *; repeat rewrite Zplus_assoc.
    repeat rewrite Zopp_plus_distr; repeat rewrite Zopp_involutive.
    rewrite (Zplus_comm (a + b) (- (m × ((a + b) / m)))).
    repeat rewrite <- Zplus_assoc.
    apply Zdivides_plus_elim.
     auto with zarith.
    rewrite (Zplus_assoc (m × (a / m)) (- b) (m × (b / m))).
    rewrite (Zplus_comm (m × (a / m)) (- b)).
    rewrite <- (Zplus_assoc (- b) (m × (a / m)) (m × (b / m))).
    rewrite (Zplus_assoc (- a) (- b) (m × (a / m) + m × (b / m))).
    rewrite <- Zopp_plus_distr.
    repeat rewrite Zplus_assoc.
    rewrite Zplus_opp_r.
    auto with zarith.
   generalize (Z_div_mod_eq (a + b) m Hm); auto with zarith.
  generalize (Z_div_mod_eq b m Hm); auto with zarith.
 generalize (Z_div_mod_eq a m Hm); auto with zarith.
Qed.

Lemma Zmod_plus_compat_rht :
 ∀ m a b : Z, (m > 0)%Z → ((a + b) mod m)%Z = ((a + b mod m) mod m)%Z.
Proof.
 intros m a b Hm.
 rewrite (Zmod_plus_compat m a b Hm).
 rewrite <- (Zmod_Zmod m (a + b mod m) Hm).
 rewrite (Zmod_plus_compat m a (b mod m) Hm).
 rewrite Zmod_Zmod; auto.
 rewrite Zmod_Zmod; auto.
Qed.

Lemma Zmod_plus_compat_lft :
 ∀ m a b : Z, (m > 0)%Z → ((a + b) mod m)%Z = ((a mod m + b) mod m)%Z.
Proof.
 intros m a b Hm.
 rewrite (Zplus_comm a b).
 rewrite (Zplus_comm (a mod m) b).
 apply Zmod_plus_compat_rht.
 auto.
Qed.

Lemma Zmod_opp_elim :
 ∀ m a : Z, (m > 0)%Z → (- a mod m)%Z = ((m - a mod m) mod m)%Z.
Proof.
 intros m a Hm.
 apply Zmod_minus_intro.
  exact Hm.
 replace (- a - (m - a mod m))%Z with (- m + (a mod m - a))%Z; auto with zarith.
 replace (- m)%Z with (-1 × m)%Z; auto with zarith.
 rewrite Zmod_cancel_multiple; auto.
 replace (a mod m - a)%Z with (- (a / m) × m)%Z; auto with zarith.
 generalize (Z_div_mod_eq a m Hm).
 set (q := (a / m)%Z); set (r := (a mod m)%Z); intro Ha; rewrite Ha.
 rewrite Zplus_comm; unfold Zminus in |- *; rewrite Zopp_plus_distr;
   rewrite Zplus_assoc; rewrite Zplus_opp_r; rewrite Zplus_0_l;
     rewrite Zopp_mult_distr_l_reverse; rewrite Zmult_comm; reflexivity.
Qed.

Lemma Zmod_minus_elim :
 ∀ m a b : Z,
 (m > 0)%Z → (a mod m)%Z = (b mod m)%Z → ((a - b) mod m)%Z = 0%Z.
Proof.
 intros m a b Hm Heq.
 unfold Zminus in |- ×.
 rewrite (Zmod_plus_compat m a (- b) Hm).
 rewrite Heq.
 rewrite Zmod_opp_elim; auto.
 rewrite <- (Zmod_plus_compat m b (m - b mod m) Hm).
 unfold Zminus in |- ×.
 rewrite Zplus_assoc.
 rewrite (Zplus_comm b m).
 rewrite <- Zplus_assoc.
 fold (b - b mod m)%Z in |- ×.
 replace (b - b mod m)%Z with (b / m × m)%Z.
  rewrite Zplus_comm.
  rewrite Zmod_cancel_multiple; auto.
  apply Zmod_same; auto.
 set (q := (b / m)%Z); set (r := (b mod m)%Z).
 rewrite (Z_div_mod_eq b m Hm).
 fold q in |- *; fold r in |- ×.
 rewrite Zmult_comm.
 unfold Zminus in |- ×.
 rewrite <- Zplus_assoc.
 rewrite Zplus_opp_r.
 auto with zarith.
Qed.

Lemma Zmod_mult_compat :
 ∀ m a b : Z,
 (m > 0)%Z → ((a × b) mod m)%Z = ((a mod m × (b mod m)) mod m)%Z.
Proof.
 intros m a b Hm.
 rewrite <- (Zmod_Zmod m (a × b) Hm).
 apply Zmod_minus_intro; auto.
 apply Zmod0_Zdivides.
  auto with zarith.
 replace (a mod m)%Z with (a - m × (a / m))%Z.
  replace (b mod m)%Z with (b - m × (b / m))%Z.
   replace ((a × b) mod m)%Z with (a × b - m × (a × b / m))%Z.
    unfold Zminus in |- *; repeat rewrite Zplus_assoc.
    repeat rewrite Zmult_plus_distr_l.
    repeat rewrite Zmult_plus_distr_r.
    repeat rewrite Zopp_plus_distr; repeat rewrite Zopp_involutive.
    rewrite (Zplus_comm (a × b)).
    repeat rewrite <- Zplus_assoc.
    apply Zdivides_plus_elim.
     auto with zarith.
    repeat rewrite Zplus_assoc.
    rewrite Zplus_opp_r.
    repeat rewrite Zopp_mult_distr_l_reverse; repeat rewrite Zopp_mult_distr_r;
      repeat rewrite Zopp_involutive.
    simpl in |- ×.
    apply Zdivides_plus_elim; auto with zarith.
   generalize (Z_div_mod_eq (a × b) m Hm); auto with zarith.
  generalize (Z_div_mod_eq b m Hm); auto with zarith.
 generalize (Z_div_mod_eq a m Hm); auto with zarith.
Qed.

Lemma Zmod_mult_compat_rht :
 ∀ m a b : Z, (m > 0)%Z → ((a × b) mod m)%Z = ((a × (b mod m)) mod m)%Z.
Proof.
 intros m a b Hm.
 rewrite (Zmod_mult_compat m a b Hm).
 rewrite <- (Zmod_Zmod m (a × (b mod m)) Hm).
 rewrite (Zmod_mult_compat m a (b mod m) Hm).
 rewrite Zmod_Zmod; auto.
 rewrite Zmod_Zmod; auto.
Qed.

Lemma Zmod_mult_compat_lft :
 ∀ m a b : Z, (m > 0)%Z → ((a × b) mod m)%Z = ((a mod m × b) mod m)%Z.
Proof.
 intros m a b Hm.
 rewrite (Zmult_comm a b).
 rewrite (Zmult_comm (a mod m) b).
 apply Zmod_mult_compat_rht.
 auto.
Qed.

Lemma Zmod_mult_elim_lft :
 ∀ m a b c : Z,
 (m > 0)%Z →
 Zrelprime a m →
 ((a × b) mod m)%Z = ((a × c) mod m)%Z → (b mod m)%Z = (c mod m)%Z.
Proof.
 intros m a b c Hm Hrelprime Hmulteq.
 assert (Hm0 : m ≠ 0%Z); auto with zarith.
 generalize (Zdivides_Zmod0 _ _ Hm0 (Zmod_minus_elim m _ _ Hm Hmulteq)); intro Hdiv.
 rewrite (Zmult_comm a b) in Hdiv; rewrite (Zmult_comm a c) in Hdiv;
   rewrite <- BinInt.Zmult_minus_distr_r in Hdiv.
 apply Zmod_minus_intro; auto.
 apply Zmod0_Zdivides. auto with zarith.
  apply (Zrelprime_div_mult_intro m a (b - c)).
  apply Zrelprime_symm; assumption.
 rewrite Zmult_comm; assumption.
Qed.

Lemma Zmod_mult_elim_rht :
 ∀ m a b c : Z,
 (m > 0)%Z →
 Zrelprime a m →
 ((b × a) mod m)%Z = ((c × a) mod m)%Z → (b mod m)%Z = (c mod m)%Z.
 intros m a b c; rewrite (Zmult_comm b a); rewrite (Zmult_comm c a); apply Zmod_mult_elim_lft.
Qed.

Lemma Zmod_opp_zero :
 ∀ m a : Z, (m > 0)%Z → (a mod m)%Z = 0%Z → (- a mod m)%Z = 0%Z.
Proof.
 intros m a Hm Ha.
 rewrite (Zmod_opp_elim m a Hm).
 rewrite Ha.
 unfold Zminus in |- *; simpl in |- *; rewrite Zplus_0_r.
 apply (Z_mod_same m Hm).
Qed.

Lemma Zmod_small :
 ∀ m a : Z, (m > 0)%Z → (0 ≤ a < m)%Z → (a mod m)%Z = a.
Proof.
 intros m a Hm Ha.
 apply (Zmodeq_small (a mod m) a m).
   apply (Z_mod_lt a m Hm).
  exact Ha.
 replace (a mod m - a)%Z with (- m × (a / m))%Z.
  auto with zarith.
 generalize (Z_div_mod_eq a m Hm).
 set (q := (a / m)%Z); set (r := (a mod m)%Z); intro H; rewrite H.
 rewrite Zplus_comm; unfold Zminus in |- *; rewrite Zopp_plus_distr;
   rewrite Zplus_assoc; rewrite Zplus_opp_r; rewrite Zplus_0_l;
     rewrite Zopp_mult_distr_l_reverse; rewrite Zmult_comm; reflexivity.
Qed.

Lemma Zmod_opp_nonzero :
 ∀ m a : Z,
 (m > 0)%Z → (a mod m)%Z ≠ 0%Z → (- a mod m)%Z = (m - a mod m)%Z.
Proof.
 intros m a Hm Ha.
 rewrite (Zmod_opp_elim m a Hm).
 apply Zmod_small.
  exact Hm.
 generalize (Z_mod_lt a m Hm); intro Hlt.
 auto with zarith.
Qed.

Lemma Zmod_one_lft : ∀ m : Z, (m > 1)%Z → (1 mod m)%Z = 1%Z.
Proof.
 intros m Hm.
 apply Zmod_small; auto with zarith.
Qed.

Lemma Zmod_one_rht : ∀ a : Z, (a mod 1)%Z = 0%Z.
Proof.
 intro a.
 generalize (Z_mod_lt a 1).
 auto with zarith.
Qed.

Lemma Zmod_lin_comb :
 ∀ m a : Z,
 (m > 0)%Z → (Zgcd a m < m)%Z → ((a × Zgcd_coeff_a a m) mod m)%Z = Zgcd a m.
Proof.
 intros m a Hm Hgcd.
 generalize (Zgcd_lin_comb a m); intro Hlincomb.
 rewrite (Z_div_mod_eq (Zgcd_coeff_a a m × a) m Hm) in Hlincomb.
 rewrite Zmult_comm in Hlincomb.
 rewrite Zplus_comm in Hlincomb.
 rewrite Zplus_assoc in Hlincomb.
 rewrite <- Zmult_plus_distr_l in Hlincomb.
 replace (Zgcd a m) with (Zgcd a m mod m)%Z.
  rewrite Hlincomb.
  rewrite Zmod_plus_compat; auto.
  rewrite Zmod_Zmod; auto.
  rewrite <- Zmod_plus_compat; auto.
  apply Zmod_minus_intro; auto.
  set (u := Zgcd_coeff_a a m).
  set (v := Zgcd_coeff_b a m).
  rewrite (Zplus_comm ((v + u × a / m) × m) (u × a)).
  unfold Zminus in |- ×.
  rewrite Zopp_plus_distr.
  rewrite Zplus_assoc.
  rewrite (Zmult_comm a u).
  rewrite Zplus_opp_r.
  rewrite Zplus_0_l.
  rewrite <- Zopp_mult_distr_l_reverse.
  apply Zmod_multiple; auto.
 apply Zmod_small; auto.
 auto with zarith.
Qed.

Lemma Zmod_relprime_inv :
 ∀ m a : Z,
 (m > 1)%Z → Zrelprime a m → ((a × Zgcd_coeff_a a m) mod m)%Z = 1%Z.
Proof.
 intros m a Hm H1.
 unfold Zrelprime in H1.
 generalize (Zgcd_lin_comb a m).
 intro Hlc.
 rewrite H1 in Hlc.
 rewrite (Zmult_comm (Zgcd_coeff_a a m) a) in Hlc.
 assert (Hqr : (a × Zgcd_coeff_a a m)%Z = (- Zgcd_coeff_b a m × m + 1)%Z).
  rewrite Zplus_comm.
  rewrite Hlc.
  rewrite <- Zplus_assoc.
  rewrite Zopp_mult_distr_l_reverse.
  auto with zarith.
 generalize (Z_div_mod_eq (a × Zgcd_coeff_a a m) m); intro Hdivmod;
   assert (Hm0 : (m > 0)%Z); auto with zarith; generalize (Hdivmod Hm0); clear Hdivmod; intro Hdivmod.
 rewrite (Zmult_comm m (a × Zgcd_coeff_a a m / m)) in Hdivmod.
 apply (Zdiv_remainder_unique _ _ _ _ (- Zgcd_coeff_b a m) 1 Hdivmod).
   apply Z_mod_lt.
   auto with zarith.
  exact Hqr.
 auto with zarith.
Qed.

End zmod.

Hint Resolve Zmod_zero_lft: zarith.
Hint Resolve Zmod_zero_rht: zarith.
Hint Resolve Zmod_same: zarith.
Hint Resolve Zmod_Zmod: zarith.
Hint Resolve Zmod_cancel_multiple: zarith.
Hint Resolve Zmod_multiple: zarith.
Hint Resolve Zmod_minus_intro: zarith.
Hint Resolve Zmod_plus_compat: zarith.
Hint Resolve Zmod_plus_compat_lft: zarith.
Hint Resolve Zmod_plus_compat_rht: zarith.
Hint Resolve Zmod_opp_elim: zarith.
Hint Resolve Zmod_minus_elim: zarith.
Hint Resolve Zmod_mult_compat: zarith.
Hint Resolve Zmod_mult_compat_lft: zarith.
Hint Resolve Zmod_mult_compat_rht: zarith.
Hint Resolve Zmod_opp_zero: zarith.
Hint Resolve Zmod_small: zarith.
Hint Resolve Zmod_opp_nonzero: zarith.
Hint Resolve Zmod_one_lft: zarith.
Hint Resolve Zmod_one_rht: zarith.
Hint Resolve Zmod_lin_comb: zarith.
Hint Resolve Zmod_relprime_inv: zarith.


Section zmodeq.

Variable m : positive.

Definition Zmodeq (a b : Z) := Zdivides m (a - b).

Lemma Zmodeq_dec : ∀ a b : Z, {Zmodeq a b} + {¬ Zmodeq a b}.
Proof.
 intros a b.
 unfold Zmodeq in |- ×.
 apply Zdivides_dec.
Qed.

Lemma Zmodeq_modeq : ∀ a b : Z, Zmodeq a b → (a mod m)%Z = (b mod m)%Z.
Proof.
 intros a b H.
 apply Zmod_minus_intro.
  auto with zarith.
 unfold Zmodeq in H.
 apply Zmod0_Zdivides.
  intro Hfalse; inversion Hfalse.
 assumption.
Qed.

Lemma Zmodeq_eqmod : ∀ a b : Z, (a mod m)%Z = (b mod m)%Z → Zmodeq a b.
Proof.
 intros a b H.
 unfold Zmodeq in |- ×.
 apply Zdivides_Zmod0.
  intro Hfalse; inversion Hfalse.
 apply Zmod_minus_elim; auto with zarith.
Qed.

Lemma Zmodeq_refl : ∀ a : Z, Zmodeq a a.
Proof.
 intros.
 unfold Zmodeq in |- ×.
 unfold Zminus in |- ×.
 rewrite Zplus_opp_r.
 apply Zdivides_zero_rht.
Qed.

Lemma Zmodeq_symm : ∀ a b : Z, Zmodeq a b → Zmodeq b a.
Proof.
 unfold Zmodeq in |- ×.
 intros.
 replace (b - a)%Z with (- (a - b))%Z; auto with zarith.
Qed.

Lemma Zmodeq_trans : ∀ a b c : Z, Zmodeq b a → Zmodeq a c → Zmodeq b c.
Proof.
 unfold Zmodeq in |- ×.
 intros.
 replace (b - c)%Z with (b - a + (a - c))%Z; auto with zarith.
Qed.

Lemma Zmodeq_zero : ∀ a : Z, Zmodeq a 0 ↔ Zdivides m a.
Proof.
 unfold Zmodeq in |- *; unfold Zdivides in |- ×.
 intros.
 unfold Zminus in |- ×.
 simpl in |- ×.
 rewrite Zplus_0_r.
 tauto.
Qed.

Lemma Zmodeq_rem : ∀ a : Z, Zmodeq a (a mod m).
Proof.
 intros.
 unfold Zmodeq in |- ×.
 ∃ (a / m)%Z.
 rewrite Zmult_comm.
 generalize (Z_div_mod_eq a m).
 cut (m > 0)%Z; auto with zarith.
Qed.

Lemma Zmodeq_plus_compat :
 ∀ a b c d : Z, Zmodeq a b → Zmodeq c d → Zmodeq (a + c) (b + d).
Proof.
 intros a b c d.
 unfold Zmodeq in |- ×.
 unfold Zdivides in |- ×.
 intros Hab Hcd.
 elim Hab.
 intros q1 H1.
 elim Hcd.
 intros q2 H2.
 ∃ (q1 + q2)%Z.
 rewrite Zmult_plus_distr_l.
 auto with zarith.
Qed.

Definition Zmodeq_plus_elim := Zmodeq_plus_compat.

Lemma Zmodeq_plus_elim_lft :
 ∀ a b c : Z, Zmodeq a b → Zmodeq (c + a) (c + b).
Proof.
 intros.
 apply Zmodeq_plus_compat.
  apply Zmodeq_refl.
 assumption.
Qed.

Lemma Zmodeq_plus_elim_rht :
 ∀ a b c : Z, Zmodeq a b → Zmodeq (a + c) (b + c).
Proof.
 intros.
 apply Zmodeq_plus_compat.
  assumption.
 apply Zmodeq_refl.
Qed.

Lemma Zmodeq_mult_elim_lft :
 ∀ a b c : Z, Zmodeq a b → Zmodeq (c × a) (c × b).
Proof.
 intros.
 unfold Zmodeq in |- ×.
 unfold Zminus in |- ×.
 rewrite (Zmult_comm c b).
 rewrite <- Zopp_mult_distr_l_reverse.
 rewrite (Zmult_comm c a).
 rewrite <- Zmult_plus_distr_l.
 fold (a - b)%Z in |- ×.
 apply Zdivides_mult_elim_rht.
 assumption.
Qed.

Lemma Zmodeq_mult_elim_rht :
 ∀ a b c : Z, Zmodeq a b → Zmodeq (a × c) (b × c).
Proof.
 intros.
 rewrite (Zmult_comm a c).
 rewrite (Zmult_comm b c).
 apply Zmodeq_mult_elim_lft.
 assumption.
Qed.

Lemma Zmodeq_mult_compat :
 ∀ a b c d : Z, Zmodeq a b → Zmodeq c d → Zmodeq (a × c) (b × d).
Proof.
 intros a b c d Hab Hcd.
 apply (Zmodeq_trans (b × c)).
  apply Zmodeq_mult_elim_rht; assumption.
 apply Zmodeq_mult_elim_lft; assumption.
Qed.

Definition Zmodeq_mult_elim := Zmodeq_mult_compat.

Lemma Zmodeq_opp_elim : ∀ a b : Z, Zmodeq a b → Zmodeq (- a) (- b).
Proof.
 intros a b H.
 replace (- a)%Z with (-1 × a)%Z; auto with zarith.
 replace (- b)%Z with (-1 × b)%Z; auto with zarith.
 apply Zmodeq_mult_elim.
  apply Zmodeq_refl.
 exact H.
Qed.

Lemma Zmodeq_opp_intro : ∀ a b : Z, Zmodeq (- a) (- b) → Zmodeq a b.
Proof.
 intros a b H.
 rewrite <- (Zopp_involutive a).
 rewrite <- (Zopp_involutive b).
 apply (Zmodeq_opp_elim _ _ H).
Qed.

Lemma Zmodeq_gcd_compat_lft :
 ∀ a b : Z, Zmodeq a b → Zgcd m a = Zgcd m b.
Proof.
 unfold Zmodeq in |- ×.
 intros a b H0.
 elim H0; intros q Hq.
 replace (Zgcd m b) with (Zgcd m (b + q × m)); auto with zarith.
 rewrite Hq.
 replace (b + (a - b))%Z with a; auto with zarith.
Qed.

Lemma Zmodeq_gcd_compat_rht :
 ∀ a b : Z, Zmodeq a b → Zgcd a m = Zgcd b m.
Proof.
 intros.
 rewrite (Zgcd_symm a m).
 rewrite (Zgcd_symm b m).
 apply Zmodeq_gcd_compat_lft.
 assumption.
Qed.

Lemma Zmodeq_relprime :
 ∀ a b : Z, Zmodeq a b → Zrelprime a m → Zrelprime b m.
Proof.
 intros a b H.
 unfold Zrelprime in |- ×.
 rewrite (Zmodeq_gcd_compat_rht a b H).
 tauto.
Qed.

Lemma Zmodeq_mod_elim :
 ∀ a b : Z, Zmodeq a b → Zmodeq (a mod m) (b mod m).
Proof.
 intros a b H.
 apply Zmodeq_eqmod.
 rewrite Zmod_Zmod; auto with zarith.
 rewrite Zmod_Zmod; auto with zarith.
Qed.

Lemma Zmodeq_mod_elim_lft : ∀ a b : Z, Zmodeq a b → Zmodeq (a mod m) b.
Proof.
 intros a b H.
 apply Zmodeq_eqmod.
 rewrite Zmod_Zmod; auto with zarith.
Qed.

Lemma Zmodeq_mod_elim_rht : ∀ a b : Z, Zmodeq a b → Zmodeq a (b mod m).
Proof.
 intros a b H.
 apply Zmodeq_eqmod.
 rewrite Zmod_Zmod; auto with zarith.
Qed.

Lemma Zmodeq_mod_intro :
 ∀ a b : Z, Zmodeq (a mod m) (b mod m) → Zmodeq a b.
Proof.
 intros a b H.
 apply Zmodeq_eqmod.
 rewrite <- (Zmod_Zmod m a); auto with zarith.
 rewrite <- (Zmod_Zmod m b); auto with zarith.
Qed.

Lemma Zmodeq_mod_intro_lft : ∀ a b : Z, Zmodeq (a mod m) b → Zmodeq a b.
Proof.
 intros a b H.
 apply Zmodeq_eqmod.
 rewrite <- (Zmod_Zmod m a); auto with zarith.
Qed.

Lemma Zmodeq_mod_intro_rht : ∀ a b : Z, Zmodeq a (b mod m) → Zmodeq a b.
Proof.
 intros a b H.
 apply Zmodeq_eqmod.
 rewrite <- (Zmod_Zmod m b); auto with zarith.
Qed.

End zmodeq.

Hint Resolve Zmodeq_dec: zarith.
Hint Resolve Zmodeq_modeq: zarith.
Hint Resolve Zmodeq_eqmod: zarith.
Hint Resolve Zmodeq_refl: zarith.
Hint Resolve Zmodeq_symm: zarith.
Hint Resolve Zmodeq_trans: zarith.
Hint Resolve Zmodeq_zero: zarith.
Hint Resolve Zmodeq_rem: zarith.
Hint Resolve Zmodeq_plus_compat: zarith.
Hint Resolve Zmodeq_plus_elim: zarith.
Hint Resolve Zmodeq_plus_elim_lft: zarith.
Hint Resolve Zmodeq_plus_elim_rht: zarith.
Hint Resolve Zmodeq_mult_elim_lft: zarith.
Hint Resolve Zmodeq_mult_elim_rht: zarith.
Hint Resolve Zmodeq_mult_compat: zarith.
Hint Resolve Zmodeq_mult_elim: zarith.
Hint Resolve Zmodeq_opp_intro: zarith.
Hint Resolve Zmodeq_opp_elim: zarith.
Hint Resolve Zmodeq_gcd_compat_lft: zarith.
Hint Resolve Zmodeq_gcd_compat_rht: zarith.
Hint Resolve Zmodeq_relprime: zarith.
Hint Resolve Zmodeq_mod_elim: zarith.
Hint Resolve Zmodeq_mod_elim_lft: zarith.
Hint Resolve Zmodeq_mod_elim_rht: zarith.
Hint Resolve Zmodeq_mod_intro: zarith.
Hint Resolve Zmodeq_mod_intro_lft: zarith.
Hint Resolve Zmodeq_mod_intro_rht: zarith.