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.toFin = d.toFin

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).toFin = ⟨n, h⟩

@[simp]

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

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

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.toFin + ↑m.toFin < size) : n.toNat + m.toNat = (n + m).toNat

theorem UInt32.toNat_sub_toNat {n m : UInt32} (hmn : m.toFin ≤ n.toFin) (h2 : ↑n.toFin < 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.toFin < 1114112

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

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

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

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

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

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