Add Z.mul_split

2 files changed, 12 insertions, 0 deletions

diff --git a/src/Util/ZUtil/Definitions.v b/src/Util/ZUtil/Definitions.v
index 6fc969dfd..ff15dc83c 100644
--- a/src/Util/ZUtil/Definitions.v
+++ b/src/Util/ZUtil/Definitions.v
@@ -35,4 +35,6 @@ Module Z.
        then add_get_carry (Z.log2 bound) x y
        else ((x + y) mod bound, (x + y) / bound).
 
+  Definition mul_split (s x y : Z) : Z * Z
+    := ((x * y) mod s, (x * y) / s).
 End Z.
diff --git a/src/Util/ZUtil/MulSplit.v b/src/Util/ZUtil/MulSplit.v
new file mode 100644
index 000000000..e0448fe69
--- /dev/null
+++ b/src/Util/ZUtil/MulSplit.v
@@ -0,0 +1,10 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.ZUtil.Definitions.
+Local Open Scope Z_scope.
+
+Module Z.
+  Lemma mul_split_mod s x y : fst (Z.mul_split s x y)  = (x * y) mod s.
+  Proof. reflexivity. Qed.
+  Lemma mul_split_div s x y : snd (Z.mul_split s x y)  = (x * y) / s.
+  Proof. reflexivity. Qed.
+End Z.