feat: add BitVec.(shiftLeft_add_distrib, shiftLeft_ushiftRight)

src/Init/Data/BitVec/Lemmas.lean

@@ -1512,6 +1512,25 @@ theorem shiftRight_add {w : Nat} (x : BitVec w) (n m : Nat) :
   ext i
   simp [Nat.add_assoc n m i]
 
+@[simp]
+theorem shiftLeft_ushiftRight {x : BitVec w} {n : Nat}:
+  x >>> n <<< n = x &&& BitVec.allOnes w <<< n := by
+  induction n generalizing x
+  case zero =>
+    ext; simp
+  case succ n ih =>
+    rw [BitVec.shiftLeft_add, Nat.add_comm, BitVec.shiftRight_add, ih,
+       Nat.add_comm, BitVec.shiftLeft_add, BitVec.shiftLeft_and_distrib]
+    ext i
+    have hi₁ (_: 0 < i.val) : 1 + (i.val - 1) = i := by
+      rw [Nat.add_comm, Nat.sub_add_cancel]
+      omega
+    by_cases hw : w = 0
+    · simp [hw]
+    by_cases hi₂ : i.val = 0
+    · simp [hi₂]
+    · simp [Nat.lt_one_iff, hi₂, hi₁ (show 0 < i.val by omega)]
+
 @[deprecated shiftRight_add (since := "2024-06-02")]
 theorem shiftRight_shiftRight {w : Nat} (x : BitVec w) (n m : Nat) :
     (x >>> n) >>> m = x >>> (n + m) := by
@@ -1737,6 +1756,15 @@ theorem ofInt_add {n} (x y : Int) : BitVec.ofInt n (x + y) =
   apply eq_of_toInt_eq
   simp
 
+@[simp]
+theorem shiftLeft_add_distrib {x y : BitVec w} {n : Nat} :
+    (x + y) <<< n = x <<< n + y <<< n := by
+  induction n
+  case zero =>
+    simp
+  case succ n ih =>
+    simp [ih, toNat_eq, Nat.shiftLeft_eq_mul_pow, ←Nat.add_mul]
+
 /-! ### sub/neg -/
 
 theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toNat) := by rfl

src/Init/Data/Nat/Basic.lean

@@ -634,6 +634,8 @@ theorem lt_succ_of_lt (h : a < b) : a < succ b := le_succ_of_le h
 
 theorem lt_add_one_of_lt (h : a < b) : a < b + 1 := le_succ_of_le h
 
+theorem lt_one_iff : n < 1 ↔ n = 0 := Nat.lt_succ_iff.trans <| by rw [le_zero_eq]
+
 theorem succ_pred_eq_of_ne_zero : ∀ {n}, n ≠ 0 → succ (pred n) = n
   | _+1, _ => rfl
 

src/Init/Data/Nat/Lemmas.lean

@@ -605,6 +605,9 @@ theorem add_mod (a b n : Nat) : (a + b) % n = ((a % n) + (b % n)) % n := by
     | zero => simp_all
     | succ k => omega
 
+@[simp] theorem mod_mul_mod {a b c : Nat} : (a % c * b) % c = a * b % c := by
+  rw [mul_mod, mod_mod, ← mul_mod]
+
 /-! ### pow -/
 
 theorem pow_succ' {m n : Nat} : m ^ n.succ = m * m ^ n := by
@@ -916,6 +919,8 @@ theorem mul_add_mod (m x y : Nat) : (m * x + y) % m = y % m := by
   · exact (m % 0).div_zero
   · case succ n => exact Nat.div_eq_of_lt (m.mod_lt n.succ_pos)
 
+theorem shiftLeft_eq_mul_pow (m) : ∀ n, m <<< n = m * 2 ^ n := shiftLeft_eq _
+
 /-! ### Decidability of predicates -/
 
 instance decidableBallLT :