Section zmod.

Definition Zmod_same := Z_mod_same.

Lemma Zmod_zero_lft : forall m : Z, (0 mod m)%Z = 0%Z.

Lemma Zmod_zero_rht : forall a : Z, (a mod 0)%Z = 0%Z.

Lemma Zmod_Zmod :
 forall m a : Z, (m > 0)%Z -> ((a mod m) mod m)%Z = (a mod m)%Z.

Lemma Zmod_cancel_multiple :
 forall m a b : Z, (m > 0)%Z -> ((b * m + a) mod m)%Z = (a mod m)%Z.

Lemma Zmod_multiple : forall m a : Z, (m > 0)%Z -> ((a * m) mod m)%Z = 0%Z.

Lemma Zmod_minus_intro :
 forall m a b : Z,
 (m > 0)%Z -> ((a - b) mod m)%Z = 0%Z -> (a mod m)%Z = (b mod m)%Z.

Lemma Zmod_plus_compat :
 forall m a b : Z,
 (m > 0)%Z -> ((a + b) mod m)%Z = ((a mod m + b mod m) mod m)%Z.

Lemma Zmod_plus_compat_rht :
 forall m a b : Z, (m > 0)%Z -> ((a + b) mod m)%Z = ((a + b mod m) mod m)%Z.

Lemma Zmod_plus_compat_lft :
 forall m a b : Z, (m > 0)%Z -> ((a + b) mod m)%Z = ((a mod m + b) mod m)%Z.

Lemma Zmod_opp_elim :
 forall m a : Z, (m > 0)%Z -> (- a mod m)%Z = ((m - a mod m) mod m)%Z.

Lemma Zmod_minus_elim :
 forall m a b : Z,
 (m > 0)%Z -> (a mod m)%Z = (b mod m)%Z -> ((a - b) mod m)%Z = 0%Z.

Lemma Zmod_mult_compat :
 forall m a b : Z,
 (m > 0)%Z -> ((a * b) mod m)%Z = ((a mod m * (b mod m)) mod m)%Z.

Lemma Zmod_mult_compat_rht :
 forall m a b : Z, (m > 0)%Z -> ((a * b) mod m)%Z = ((a * (b mod m)) mod m)%Z.

Lemma Zmod_mult_compat_lft :
 forall m a b : Z, (m > 0)%Z -> ((a * b) mod m)%Z = ((a mod m * b) mod m)%Z.

Lemma Zmod_mult_elim_lft :
 forall 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.


Lemma Zmod_mult_elim_rht :
 forall 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.

Lemma Zmod_opp_zero :
 forall m a : Z, (m > 0)%Z -> (a mod m)%Z = 0%Z -> (- a mod m)%Z = 0%Z.

Lemma Zmod_small :
 forall m a : Z, (m > 0)%Z -> (0 <= a < m)%Z -> (a mod m)%Z = a.

Lemma Zmod_opp_nonzero :
 forall m a : Z,
 (m > 0)%Z -> (a mod m)%Z <> 0%Z -> (- a mod m)%Z = (m - a mod m)%Z.

Lemma Zmod_one_lft : forall m : Z, (m > 1)%Z -> (1 mod m)%Z = 1%Z.

Lemma Zmod_one_rht : forall a : Z, (a mod 1)%Z = 0%Z.

Lemma Zmod_lin_comb :
 forall m a : Z,
 (m > 0)%Z -> (Zgcd a m < m)%Z -> ((a * Zgcd_coeff_a a m) mod m)%Z = Zgcd a m.

Lemma Zmod_relprime_inv :
 forall m a : Z,
 (m > 1)%Z -> Zrelprime a m -> ((a * Zgcd_coeff_a a m) mod m)%Z = 1%Z.

End zmod.



Section zmodeq.

Variable m : positive.

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

Lemma Zmodeq_dec : forall a b : Z, {Zmodeq a b} + {~ Zmodeq a b}.

Lemma Zmodeq_modeq : forall a b : Z, Zmodeq a b -> (a mod m)%Z = (b mod m)%Z.

Lemma Zmodeq_eqmod : forall a b : Z, (a mod m)%Z = (b mod m)%Z -> Zmodeq a b.

Lemma Zmodeq_refl : forall a : Z, Zmodeq a a.

Lemma Zmodeq_symm : forall a b : Z, Zmodeq a b -> Zmodeq b a.

Lemma Zmodeq_trans : forall a b c : Z, Zmodeq b a -> Zmodeq a c -> Zmodeq b c.

Lemma Zmodeq_zero : forall a : Z, Zmodeq a 0 <-> Zdivides m a.

Lemma Zmodeq_rem : forall a : Z, Zmodeq a (a mod m).

Lemma Zmodeq_plus_compat :
 forall a b c d : Z, Zmodeq a b -> Zmodeq c d -> Zmodeq (a + c) (b + d).

Definition Zmodeq_plus_elim := Zmodeq_plus_compat.

Lemma Zmodeq_plus_elim_lft :
 forall a b c : Z, Zmodeq a b -> Zmodeq (c + a) (c + b).

Lemma Zmodeq_plus_elim_rht :
 forall a b c : Z, Zmodeq a b -> Zmodeq (a + c) (b + c).

Lemma Zmodeq_mult_elim_lft :
 forall a b c : Z, Zmodeq a b -> Zmodeq (c * a) (c * b).

Lemma Zmodeq_mult_elim_rht :
 forall a b c : Z, Zmodeq a b -> Zmodeq (a * c) (b * c).

Lemma Zmodeq_mult_compat :
 forall a b c d : Z, Zmodeq a b -> Zmodeq c d -> Zmodeq (a * c) (b * d).

Definition Zmodeq_mult_elim := Zmodeq_mult_compat.

Lemma Zmodeq_opp_elim : forall a b : Z, Zmodeq a b -> Zmodeq (- a) (- b).

Lemma Zmodeq_opp_intro : forall a b : Z, Zmodeq (- a) (- b) -> Zmodeq a b.

Lemma Zmodeq_gcd_compat_lft :
 forall a b : Z, Zmodeq a b -> Zgcd m a = Zgcd m b.

Lemma Zmodeq_gcd_compat_rht :
 forall a b : Z, Zmodeq a b -> Zgcd a m = Zgcd b m.

Lemma Zmodeq_relprime :
 forall a b : Z, Zmodeq a b -> Zrelprime a m -> Zrelprime b m.

Lemma Zmodeq_mod_elim :
 forall a b : Z, Zmodeq a b -> Zmodeq (a mod m) (b mod m).

Lemma Zmodeq_mod_elim_lft : forall a b : Z, Zmodeq a b -> Zmodeq (a mod m) b.

Lemma Zmodeq_mod_elim_rht : forall a b : Z, Zmodeq a b -> Zmodeq a (b mod m).

Lemma Zmodeq_mod_intro :
 forall a b : Z, Zmodeq (a mod m) (b mod m) -> Zmodeq a b.

Lemma Zmodeq_mod_intro_lft : forall a b : Z, Zmodeq (a mod m) b -> Zmodeq a b.

Lemma Zmodeq_mod_intro_rht : forall a b : Z, Zmodeq a (b mod m) -> Zmodeq a b.

End zmodeq.