1 files changed, 48 insertions, 0 deletions
diff --git a/theories/Numbers/Integer/BigInts/Zeqmod.v b/theories/Numbers/Integer/BigInts/Zeqmod.v
new file mode 100644
index 000000000..ca3286211
--- /dev/null
+++ b/theories/Numbers/Integer/BigInts/Zeqmod.v
@@ -0,0 +1,48 @@
+Require Import ZArith.
+Require Import ZAux.
+
+Open Local Scope Z_scope.
+Notation "x == y '[' 'mod' z ']'" := ((x mod z) = (y mod z))
+  (at level 70, no associativity) : Z_scope.
+
+Theorem Zeqmod_refl : forall p n : Z, n == n [mod p].
+Proof.
+reflexivity.
+Qed.
+
+Theorem Zeqmod_symm : forall p n m : Z, n == m [mod p] -> m == n [mod p].
+Proof.
+now symmetry.
+Qed.
+
+Theorem Zeqmod_trans :
+  forall p n m k : Z, n == m [mod p] -> m == k [mod p] -> n == k [mod p].
+Proof.
+intros p n m k H1 H2; now transitivity (m mod p).
+Qed.
+
+Theorem Zplus_eqmod_compat_l :
+  forall p n m k : Z, 0 < p -> (n == m [mod p] <-> k + n == k + m [mod p]).
+intros p n m k H1.
+assert (LR : forall n' m' k' : Z, n' == m' [mod p] -> k' + n' == k' + m' [mod p]).
+intros n' m' k' H2.
+pattern ((k' + n') mod p); rewrite Zmod_plus; [| assumption].
+pattern ((k' + m') mod p); rewrite Zmod_plus; [| assumption].
+rewrite H2. apply Zeqmod_refl.
+split; [apply LR |].
+intro H2. apply (LR (k + n) (k + m) (-k)) in H2.
+do 2 rewrite Zplus_assoc in H2. rewrite Zplus_opp_l in H2.
+now do 2 rewrite Zplus_0_l in H2.
+Qed.
+
+Theorem Zplus_eqmod_compat_r :
+  forall p n m k : Z, 0 < p -> (n == m [mod p] <-> n + k == m + k [mod p]).
+intros p n m k; rewrite (Zplus_comm n k); rewrite (Zplus_comm m k);
+apply Zplus_eqmod_compat_l.
+Qed.
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)