diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 59e7e4749e..f05555b3e7 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/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} :