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

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

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

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

theorem UInt32.lt_toNat_lt {a : UInt32} {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 < UInt32.size) : (UInt32.ofNat n).val = ⟨n, h⟩

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

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

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

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

theorem UInt32.toUInt32_one_add (c : Nat) (h : c + 1 < UInt32.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 < UInt32.size

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

theorem UInt32.isValidChar_pred_lt_uintSize (u : UInt32) (h2 : u.isValidChar) (h3 : 1 ≤ u) : ↑u.val - 1 < UInt32.size

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

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

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