theorem UInt32.add_def' {a b : UInt32} : a.add b = a + b

theorem UInt32.sub_def' {a b : UInt32} : a.sub b = a - b

theorem UInt32.val_ne_of_ne {c d : UInt32} (h : ¬c = d) : ¬c.val = d.val

theorem UInt32.one_le_of_lt {c1 c2 : UInt32} (h : c1 < c2) : 1 ≤ c2

theorem UInt32.lt_toNat_lt {a b : UInt32} (h : a < b) : a.toNat < b.toNat

theorem UInt32.toNat_toUInt_eq (u : UInt32) : u.toNat.toUInt32 = u

theorem UInt32.ofNat_eq (n : Nat) (h : n < size) : (ofNat n).val = ⟨n, h⟩

@[simp]

theorem UInt32.toBitVecToNat_eq_val {u : UInt32} : u.toBitVec.toNat = ↑u.val

theorem UInt32.toBitVec_add_ofNat_eq {n m : Nat} : (ofNat n).toBitVec + (ofNat m).toBitVec = BitVec.ofNat 32 (↑(ofNat n).val + ↑(ofNat m).val)

theorem UInt32.ofNat_add_ofNat (n m : Nat) (hnm : n + m < size) : ofNat n + ofNat m = ofNat (n + m)

theorem UInt32.toNat_add_toNat (n m : UInt32) (hnm : ↑n.val + ↑m.val < size) : n.toNat + m.toNat = (n + m).toNat

theorem UInt32.toNat_sub_toNat {n m : UInt32} (hmn : m.val ≤ n.val) (h2 : ↑n.val < size) : n.toNat - m.toNat = (n - m).toNat

theorem UInt32.toUInt32_add_toUInt32 (n m : Nat) (hnm : n + m < size) : n.toUInt32 + m.toUInt32 = (n + m).toUInt32

theorem UInt32.toUInt32_one_add (c : Nat) (h : c + 1 < size) : c.toUInt32 + 1 = (c + 1).toUInt32

theorem UInt32.isValidChar_lt_0x110000 (u : UInt32) (h : u.isValidChar) : ↑u.val < 1114112

theorem UInt32.isValidChar_lt_uintSize (u : UInt32) : ↑u.val < size

theorem UInt32.isValidChar_succ_lt_uintSize (u : UInt32) (h : u.isValidChar) : ↑u.val + 1 < size

theorem UInt32.isValidChar_pred_lt_uintSize (u : UInt32) : ↑u.val - 1 < size

theorem UInt32.lt_succ_le {c1 c2 : UInt32} (h : c1 < c2) (hsucc : ↑c1.val + 1 < size) : c1 + 1 ≤ c2

theorem UInt32.toNatUnfold (c1 c2 : UInt32) (heq : c2.toNat - c1.toNat = (c2 - c1).toNat) : ↑c2.val - ↑c1.val = ↑(c2 - c1).val

theorem UInt32.lt_pred_le {c1 c2 : UInt32} (h : c1 < c2) (h2 : ↑c2.val < size) : c1 ≤ c2 - 1