Michael Sammler · Michael Sammler
--- a/theories/bitvector.v 0 → 100644
+++ b/theories/bitvector.v 0 → 100644
+  induction Hall as [|b bs Hb ? IH]; [done|]; simpl.
+  apply Z_bounded_iff_bits_nonneg'; [ nia | |].
+  - apply Z.lor_nonneg. split; [|lia]. apply Z.shiftl_nonneg. lia.
+  - intros l ?. rewrite Z.lor_spec.
+    eapply Z_bounded_iff_bits_nonneg' in Hb.
+    + erewrite Hb, orb_false_r.
+      rewrite Z.shiftl_spec by nia.
+      eapply Z_bounded_iff_bits_nonneg'; [| | done |]; nia.
+    + lia.
+    + lia.
+    + nia.
+Qed.
+
+
+(** * Preliminary definitions *)
+Definition bv_modulus (n : N) : Z := 2 ^ (Z.of_N n).