Add missing file.

1 files changed, 34 insertions, 0 deletions

diff --git a/src/common/ZExtra.v b/src/common/ZExtra.v
new file mode 100644
index 0000000..a0dd717
--- /dev/null
+++ b/src/common/ZExtra.v
@@ -0,0 +1,34 @@
+Require Import ZArith.
+Require Import Lia.
+
+Local Open Scope Z_scope.
+
+Module ZExtra.
+
+  Lemma mod_0_bounds :
+    forall x y m,
+      0 < m ->
+      x mod m = 0 ->
+      y mod m = 0 ->
+      x <> y ->
+      x + m > y ->
+      y + m <= x.
+  Proof.
+    intros x y m.
+    intros POS XMOD YMOD NEQ H.
+    destruct (Z_le_gt_dec (y + m) x); eauto.
+
+    apply Znumtheory.Zmod_divide in YMOD; try lia.
+    apply Znumtheory.Zmod_divide in XMOD; try lia.
+    inversion XMOD as [x']; subst; clear XMOD.
+    inversion YMOD as [y']; subst; clear YMOD.
+
+    assert (x' <> y') as NEQ' by lia; clear NEQ.
+
+    rewrite <- Z.mul_succ_l in H.
+    rewrite <- Z.mul_succ_l in g.
+    apply Zmult_gt_reg_r in H;
+      apply Zmult_gt_reg_r in g; lia.
+  Qed.
+
+End ZExtra.