1 files changed, 32 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Odd.v b/src/Util/ZUtil/Odd.v
new file mode 100644
index 000000000..37b8bd443
--- /dev/null
+++ b/src/Util/ZUtil/Odd.v
@@ -0,0 +1,32 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.ZArith.Znumtheory.
+Require Import Coq.micromega.Lia.
+Local Open Scope Z_scope.
+
+Module Z.
+  Lemma prime_odd_or_2 : forall p (prime_p : prime p), p = 2 \/ Z.odd p = true.
+  Proof.
+    intros p prime_p.
+    apply Decidable.imp_not_l; try apply Z.eq_decidable.
+    intros p_neq2.
+    pose proof (Zmod_odd p) as mod_odd.
+    destruct (Sumbool.sumbool_of_bool (Z.odd p)) as [? | p_not_odd]; auto.
+    rewrite p_not_odd in mod_odd.
+    apply Zmod_divides in mod_odd; try omega.
+    destruct mod_odd as [c c_id].
+    rewrite Z.mul_comm in c_id.
+    apply Zdivide_intro in c_id.
+    apply prime_divisors in c_id; auto.
+    destruct c_id; [omega | destruct H; [omega | destruct H; auto] ].
+    pose proof (prime_ge_2 p prime_p); omega.
+  Qed.
+
+  Lemma odd_mod : forall a b, (b <> 0)%Z ->
+    Z.odd (a mod b) = if Z.odd b then xorb (Z.odd a) (Z.odd (a / b)) else Z.odd a.
+  Proof.
+    intros a b H.
+    rewrite Zmod_eq_full by assumption.
+    rewrite <-Z.add_opp_r, Z.odd_add, Z.odd_opp, Z.odd_mul.
+    case_eq (Z.odd b); intros; rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; auto using Bool.xorb_false_r.
+  Qed.
+End Z.