feat: lemmas about BitVector arithmetic inequalities (#5646)

These lemmas are peeled from `leanprover/lnsym`.
Moreover, note that these lemmas only hold when we do not have overflow
in their operands, and thus, we are able to treat the operands as if
they were 'regular' natural numbers.

---------

Co-authored-by: Tobias Grosser <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>

src/Init/Data/BitVec/Lemmas.lean

@@ -2840,6 +2840,31 @@ theorem toNat_mul_of_lt {w} {x y : BitVec w} (h : x.toNat * y.toNat < 2^w) :
     (x * y).toNat = x.toNat * y.toNat := by
   rw [BitVec.toNat_mul, Nat.mod_eq_of_lt h]
 
+
+/--
+`x ≤ y + z` if and only if `x - z ≤ y`
+when `x - z` and `y + z` do not overflow.
+-/
+theorem le_add_iff_sub_le {x y z : BitVec w}
+    (hxz : z ≤ x) (hbz : y.toNat + z.toNat < 2^w) :
+      x ≤ y + z ↔ x - z ≤ y := by
+  simp_all only [BitVec.le_def]
+  rw [BitVec.toNat_sub_of_le (by rw [BitVec.le_def]; omega),
+    BitVec.toNat_add_of_lt (by omega)]
+  omega
+
+/--
+`x - z ≤ y - z` if and only if `x ≤ y`
+when `x - z` and `y - z` do not overflow.
+-/
+theorem sub_le_sub_iff_le {x y z : BitVec w} (hxz : z ≤ x) (hyz : z ≤ y) :
+    (x - z ≤ y - z) ↔ x ≤ y := by
+  simp_all only [BitVec.le_def]
+  rw [BitVec.toNat_sub_of_le (by rw [BitVec.le_def]; omega),
+    BitVec.toNat_sub_of_le (by rw [BitVec.le_def]; omega)]
+  omega
+
+
 /-! ### Decidable quantifiers -/
 
 theorem forall_zero_iff {P : BitVec 0 → Prop} :