From 5fe9ec29c08dc2b2e8cedb7b2d63ddca08226199 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 4 Mar 2022 11:02:35 +0000
Subject: Clean up the proof further

---
 src/BitEQ.v | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/src/BitEQ.v b/src/BitEQ.v
index 4689b26..72f7d18 100644
--- a/src/BitEQ.v
+++ b/src/BitEQ.v
@@ -11,10 +11,8 @@ Record bv := Zbv { size: N; val: Z; }.
 
 Definition bvZ (b: bv) := (val b) mod (2 ^ (Z.of_N (size b))).
 
-Definition bvadd (sz: N) (a b: bv) :=
-  Zbv sz (bvZ a + bvZ b).
-
-Compute bvZ (bvadd 4%N (Zbv 3%N 5) (Zbv 3%N 5)).
+Definition bvadd (sz: N) (a b: bv) := Zbv sz (bvZ a + bvZ b).
+Definition bvmult (sz: N) (a b: bv) := Zbv sz (bvZ a * bvZ b).
 
 Lemma pow_2_div : forall p q, 0 <= p <= q -> (2 ^ p | 2 ^ q).
 Proof.
@@ -40,7 +38,6 @@ Lemma bounded_add_assoc :
     = bvZ (bvadd v (Zbv p a) (bvadd q (Zbv r b) (Zbv s c))).
 Proof.
   intros.
-  (* Zplus_mod *)
   unfold bvadd, bvZ; simpl in *.
   rewrite Zplus_mod by eauto. rewrite mod_mod_pow_2 by lia. symmetry.
   rewrite Zplus_mod by eauto.
-- 
cgit