1 files changed, 36 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Divide.v b/src/Util/ZUtil/Divide.v
new file mode 100644
index 000000000..8609db5ad
--- /dev/null
+++ b/src/Util/ZUtil/Divide.v
@@ -0,0 +1,36 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.ZArith.Znumtheory.
+Require Import Coq.micromega.Lia.
+Require Import Crypto.Util.ZUtil.Hints.Core.
+Require Import Crypto.Util.ZUtil.Div.
+Require Import Crypto.Util.ZUtil.Tactics.DivideExistsMul.
+Local Open Scope Z_scope.
+
+Module Z.
+  Lemma divide_mul_div: forall a b c (a_nonzero : a <> 0) (c_nonzero : c <> 0),
+    (a | b * (a / c)) -> (c | a) -> (c | b).
+  Proof.
+    intros ? ? ? ? ? divide_a divide_c_a; do 2 Z.divide_exists_mul.
+    rewrite divide_c_a in divide_a.
+    rewrite Z.div_mul' in divide_a by auto.
+    replace (b * k) with (k * b) in divide_a by ring.
+    replace (c * k * k0) with (k * (k0 * c)) in divide_a by ring.
+    rewrite Z.mul_cancel_l in divide_a by (intuition auto with nia; rewrite H in divide_c_a; ring_simplify in divide_a; intuition).
+    eapply Zdivide_intro; eauto.
+  Qed.
+
+  Lemma divide2_even_iff : forall n, (2 | n) <-> Z.even n = true.
+  Proof.
+    intros n; split. {
+      intro divide2_n.
+      Z.divide_exists_mul; [ | pose proof (Z.mod_pos_bound n 2); omega].
+      rewrite divide2_n.
+      apply Z.even_mul.
+    } {
+      intro n_even.
+      pose proof (Zmod_even n) as H.
+      rewrite n_even in H.
+      apply Zmod_divide; omega || auto.
+    }
+  Qed.
+End Z.