def commandDeclare_uint_theorems__ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem UInt8.ofBitVec_ofNat (n : Nat) : { toBitVec := BitVec.ofNat 8 n } = OfNat.ofNat n

@[simp]

theorem UInt8.toNat_mul (a b : UInt8) : (a * b).toNat = a.toNat * b.toNat % 2 ^ 8

theorem UInt8.toBitVec_ne_of_ne {a b : UInt8} (h : a ≠ b) : a.toBitVec ≠ b.toBitVec

theorem UInt8.mod_lt (a : UInt8) {b : UInt8} : 0 < b → a % b < b

theorem UInt8.le_iff_toNat_le {a b : UInt8} : a ≤ b ↔ a.toNat ≤ b.toNat

theorem UInt8.toNat_mod_lt {m : Nat} (u : UInt8) : 0 < m → (u % ofNat m).toNat < m

@[simp]

theorem UInt8.toBitVec_max {a b : UInt8} : (max a b).toBitVec = max a.toBitVec b.toBitVec

@[simp]

theorem UInt8.not_le {a b : UInt8} : ¬a ≤ b ↔ b < a

@[simp]

theorem UInt8.toNat_ofBitVec {a : BitVec 8} : { toBitVec := a }.toNat = a.toNat

theorem UInt8.min_def {a b : UInt8} : min a b = if a ≤ b then a else b

theorem UInt8.toBitVec_inj {a b : UInt8} : a.toBitVec = b.toBitVec ↔ a = b

theorem UInt8.le_antisymm {a b : UInt8} (h₁ : a ≤ b) (h₂ : b ≤ a) : a = b

theorem UInt8.ne_of_toBitVec_ne {a b : UInt8} (h : a.toBitVec ≠ b.toBitVec) : a ≠ b

theorem UInt8.lt_iff_toBitVec_lt {a b : UInt8} : a < b ↔ a.toBitVec < b.toBitVec

theorem UInt8.toBitVec_ofNat' (n : Nat) : (ofNat n).toBitVec = BitVec.ofNat 8 n

theorem UInt8.max_def {a b : UInt8} : max a b = if a ≤ b then b else a

@[simp]

theorem UInt8.ofNat_toNat {x : UInt8} : ofNat x.toNat = x

theorem UInt8.lt_iff_toNat_lt {a b : UInt8} : a < b ↔ a.toNat < b.toNat

theorem UInt8.one_def : 1 = { toBitVec := 1 }

@[simp]

theorem UInt8.toNat_toUInt64 (x : UInt8) : x.toUInt64.toNat = x.toNat

@[simp]

theorem UInt8.toNat_zero : toNat 0 = 0

instance UInt8.instLawfulOrderLT : Std.LawfulOrderLT UInt8

theorem UInt8.zero_def : 0 = { toBitVec := 0 }

theorem UInt8.le_antisymm_iff {a b : UInt8} : a = b ↔ a ≤ b ∧ b ≤ a

theorem UInt8.toNat.inj {a b : UInt8} : a.toNat = b.toNat → a = b

@[simp]

theorem UInt8.toNat_mod (a b : UInt8) : (a % b).toNat = a.toNat % b.toNat

theorem UInt8.ne_iff_toBitVec_ne {a b : UInt8} : a ≠ b ↔ a.toBitVec ≠ b.toBitVec

theorem UInt8.lt_trans {a b c : UInt8} : a < b → b < c → a < c

@[simp]

theorem UInt8.toBitVec_add {a b : UInt8} : (a + b).toBitVec = a.toBitVec + b.toBitVec

theorem UInt8.mod_def (a b : UInt8) : a % b = { toBitVec := a.toBitVec % b.toBitVec }

@[simp]

theorem UInt8.le_refl (a : UInt8) : a ≤ a

theorem UInt8.le_rfl {a : UInt8} : a ≤ a

theorem UInt8.toNat_ofNat_of_lt {n : Nat} (h : n < size) : toNat (OfNat.ofNat n) = n

theorem UInt8.eq_of_toBitVec_eq {a b : UInt8} (h : a.toBitVec = b.toBitVec) : a = b

@[simp]

theorem UInt8.toNat_sub_of_le (a b : UInt8) : b ≤ a → (a - b).toNat = a.toNat - b.toNat

theorem UInt8.mul_def (a b : UInt8) : a * b = { toBitVec := a.toBitVec * b.toBitVec }

@[simp]

theorem UInt8.toBitVec_sub {a b : UInt8} : (a - b).toBitVec = a.toBitVec - b.toBitVec

@[simp]

theorem UInt8.toNat_ofNat' {n : Nat} : (ofNat n).toNat = n % 2 ^ 8

@[simp]

theorem UInt8.ofNat_one : ofNat 1 = 1

@[simp]

theorem UInt8.toFin_toBitVec (x : UInt8) : x.toBitVec.toFin = x.toFin

instance UInt8.instIsLinearOrder : Std.IsLinearOrder UInt8

theorem UInt8.le_total (a b : UInt8) : a ≤ b ∨ b ≤ a

theorem UInt8.lt_asymm {a b : UInt8} : a < b → ¬b < a

@[simp]

theorem UInt8.toNat_add (a b : UInt8) : (a + b).toNat = (a.toNat + b.toNat) % 2 ^ 8

theorem UInt8.toNat_ofNat_of_lt' {n : Nat} (h : n < size) : (ofNat n).toNat = n

@[simp]

theorem UInt8.toBitVec_min {a b : UInt8} : (min a b).toBitVec = min a.toBitVec b.toBitVec

@[simp]

theorem UInt8.toNat_div (a b : UInt8) : (a / b).toNat = a.toNat / b.toNat

@[simp]

theorem UInt8.toBitVec_mod {a b : UInt8} : (a % b).toBitVec = a.toBitVec % b.toBitVec

@[simp]

theorem UInt8.toNat_toUInt32 (x : UInt8) : x.toUInt32.toNat = x.toNat

@[simp]

theorem UInt8.lt_irrefl (a : UInt8) : ¬a < a

theorem UInt8.sub_def (a b : UInt8) : a - b = { toBitVec := a.toBitVec - b.toBitVec }

theorem UInt8.ne_of_lt {a b : UInt8} (h : a < b) : a ≠ b

theorem UInt8.toFin_inj {a b : UInt8} : a.toFin = b.toFin ↔ a = b

theorem UInt8.le_trans {a b c : UInt8} : a ≤ b → b ≤ c → a ≤ c

theorem UInt8.eq_of_toFin_eq {a b : UInt8} (h : a.toFin = b.toFin) : a = b

theorem UInt8.add_def (a b : UInt8) : a + b = { toBitVec := a.toBitVec + b.toBitVec }

@[simp]

theorem UInt8.toBitVec_ofNat (n : Nat) : (OfNat.ofNat n).toBitVec = BitVec.ofNat 8 n

@[simp]

theorem UInt8.toNat_toBitVec (x : UInt8) : x.toBitVec.toNat = x.toNat

theorem UInt8.toNat_sub (a b : UInt8) : (a - b).toNat = (2 ^ 8 - b.toNat + a.toNat) % 2 ^ 8

theorem UInt8.toNat_ofNat {n : Nat} : (OfNat.ofNat n).toNat = n % 2 ^ 8

@[simp]

theorem UInt8.toFin_ofNat (n : Nat) : (OfNat.ofNat n).toFin = OfNat.ofNat n

@[simp]

theorem UInt8.toBitVec_div {a b : UInt8} : (a / b).toBitVec = a.toBitVec / b.toBitVec

@[simp]

theorem UInt8.toBitVec_neg {a : UInt8} : (-a).toBitVec = -a.toBitVec

@[simp]

theorem UInt8.toFin_val (x : UInt8) : ↑x.toFin = x.toNat

theorem UInt8.eq_iff_toBitVec_eq {a b : UInt8} : a = b ↔ a.toBitVec = b.toBitVec

@[simp]

theorem UInt8.toNat_toUSize (x : UInt8) : x.toUSize.toNat = x.toNat

@[simp]

theorem UInt8.not_lt {a b : UInt8} : ¬a < b ↔ b ≤ a

@[simp]

theorem UInt8.toBitVec_mul {a b : UInt8} : (a * b).toBitVec = a.toBitVec * b.toBitVec

theorem UInt8.toNat_lt_size (a : UInt8) : a.toNat < size

theorem UInt8.le_iff_toBitVec_le {a b : UInt8} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec

theorem UInt8.toNat_inj {a b : UInt8} : a.toNat = b.toNat ↔ a = b

@[simp]

theorem UInt8.toNat_toUInt16 (x : UInt8) : x.toUInt16.toNat = x.toNat

theorem UInt8.toBitVec_eq_of_eq {a b : UInt8} (h : a = b) : a.toBitVec = b.toBitVec

@[simp]

theorem UInt8.toNat_ofNatLT {n : Nat} {h : n < size} : (ofNatLT n h).toNat = n

@[simp]

theorem UInt8.ofBitVec_toBitVec (a : UInt8) : { toBitVec := a.toBitVec } = a

@[simp]

theorem UInt16.toNat_toUInt8 (x : UInt16) : x.toUInt8.toNat = x.toNat % 2 ^ 8

theorem UInt16.sub_def (a b : UInt16) : a - b = { toBitVec := a.toBitVec - b.toBitVec }

theorem UInt16.lt_trans {a b c : UInt16} : a < b → b < c → a < c

theorem UInt16.le_iff_toNat_le {a b : UInt16} : a ≤ b ↔ a.toNat ≤ b.toNat

theorem UInt16.toNat_ofNat_of_lt' {n : Nat} (h : n < size) : (ofNat n).toNat = n

@[simp]

theorem UInt16.toNat_mul (a b : UInt16) : (a * b).toNat = a.toNat * b.toNat % 2 ^ 16

@[simp]

theorem UInt16.toNat_ofBitVec {a : BitVec 16} : { toBitVec := a }.toNat = a.toNat

@[simp]

theorem UInt16.toNat_add (a b : UInt16) : (a + b).toNat = (a.toNat + b.toNat) % 2 ^ 16

theorem UInt16.max_def {a b : UInt16} : max a b = if a ≤ b then b else a

@[simp]

theorem UInt16.toNat_toUSize (x : UInt16) : x.toUSize.toNat = x.toNat

theorem UInt16.toNat_lt_size (a : UInt16) : a.toNat < size

@[simp]

theorem UInt16.toNat_toUInt32 (x : UInt16) : x.toUInt32.toNat = x.toNat

theorem UInt16.le_total (a b : UInt16) : a ≤ b ∨ b ≤ a

@[simp]

theorem UInt16.toBitVec_min {a b : UInt16} : (min a b).toBitVec = min a.toBitVec b.toBitVec

@[simp]

theorem UInt16.lt_irrefl (a : UInt16) : ¬a < a

@[simp]

theorem UInt16.toBitVec_neg {a : UInt16} : (-a).toBitVec = -a.toBitVec

theorem UInt16.le_antisymm_iff {a b : UInt16} : a = b ↔ a ≤ b ∧ b ≤ a

@[simp]

theorem UInt16.toFin_val (x : UInt16) : ↑x.toFin = x.toNat

theorem UInt16.lt_asymm {a b : UInt16} : a < b → ¬b < a

theorem UInt16.le_iff_toBitVec_le {a b : UInt16} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec

theorem UInt16.le_trans {a b c : UInt16} : a ≤ b → b ≤ c → a ≤ c

theorem UInt16.toBitVec_eq_of_eq {a b : UInt16} (h : a = b) : a.toBitVec = b.toBitVec

@[simp]

theorem UInt16.le_refl (a : UInt16) : a ≤ a

@[simp]

theorem UInt16.toBitVec_sub {a b : UInt16} : (a - b).toBitVec = a.toBitVec - b.toBitVec

@[simp]

theorem UInt16.toNat_toUInt64 (x : UInt16) : x.toUInt64.toNat = x.toNat

theorem UInt16.eq_iff_toBitVec_eq {a b : UInt16} : a = b ↔ a.toBitVec = b.toBitVec

@[simp]

theorem UInt16.not_lt {a b : UInt16} : ¬a < b ↔ b ≤ a

theorem UInt16.toNat_mod_lt {m : Nat} (u : UInt16) : 0 < m → (u % ofNat m).toNat < m

theorem UInt16.toBitVec_inj {a b : UInt16} : a.toBitVec = b.toBitVec ↔ a = b

theorem UInt16.mod_lt (a : UInt16) {b : UInt16} : 0 < b → a % b < b

theorem UInt16.lt_iff_toNat_lt {a b : UInt16} : a < b ↔ a.toNat < b.toNat

@[simp]

theorem UInt16.toBitVec_mul {a b : UInt16} : (a * b).toBitVec = a.toBitVec * b.toBitVec

theorem UInt16.toNat_inj {a b : UInt16} : a.toNat = b.toNat ↔ a = b

@[simp]

theorem UInt16.ofBitVec_toBitVec (a : UInt16) : { toBitVec := a.toBitVec } = a

theorem UInt16.lt_iff_toBitVec_lt {a b : UInt16} : a < b ↔ a.toBitVec < b.toBitVec

theorem UInt16.mul_def (a b : UInt16) : a * b = { toBitVec := a.toBitVec * b.toBitVec }

@[simp]

theorem UInt16.toFin_ofNat (n : Nat) : (OfNat.ofNat n).toFin = OfNat.ofNat n

@[simp]

theorem UInt16.toNat_zero : toNat 0 = 0

theorem UInt16.toNat_ofNat {n : Nat} : (OfNat.ofNat n).toNat = n % 2 ^ 16

theorem UInt16.toBitVec_ofNat' (n : Nat) : (ofNat n).toBitVec = BitVec.ofNat 16 n

@[simp]

theorem UInt16.ofNat_toNat {x : UInt16} : ofNat x.toNat = x

@[simp]

theorem UInt16.toNat_div (a b : UInt16) : (a / b).toNat = a.toNat / b.toNat

@[simp]

theorem UInt16.toNat_ofNat' {n : Nat} : (ofNat n).toNat = n % 2 ^ 16

@[simp]

theorem UInt16.toBitVec_mod {a b : UInt16} : (a % b).toBitVec = a.toBitVec % b.toBitVec

theorem UInt16.ne_of_lt {a b : UInt16} (h : a < b) : a ≠ b

@[simp]

theorem UInt16.ofNat_one : ofNat 1 = 1

@[simp]

theorem UInt16.toNat_toBitVec (x : UInt16) : x.toBitVec.toNat = x.toNat

theorem UInt16.one_def : 1 = { toBitVec := 1 }

instance UInt16.instLawfulOrderLT : Std.LawfulOrderLT UInt16

theorem UInt16.le_rfl {a : UInt16} : a ≤ a

theorem UInt16.ne_of_toBitVec_ne {a b : UInt16} (h : a.toBitVec ≠ b.toBitVec) : a ≠ b

theorem UInt16.eq_of_toFin_eq {a b : UInt16} (h : a.toFin = b.toFin) : a = b

theorem UInt16.mod_def (a b : UInt16) : a % b = { toBitVec := a.toBitVec % b.toBitVec }

theorem UInt16.toNat.inj {a b : UInt16} : a.toNat = b.toNat → a = b

theorem UInt16.eq_of_toBitVec_eq {a b : UInt16} (h : a.toBitVec = b.toBitVec) : a = b

theorem UInt16.toNat_ofNat_of_lt {n : Nat} (h : n < size) : toNat (OfNat.ofNat n) = n

@[simp]

theorem UInt16.toBitVec_add {a b : UInt16} : (a + b).toBitVec = a.toBitVec + b.toBitVec

instance UInt16.instIsLinearOrder : Std.IsLinearOrder UInt16

@[simp]

theorem UInt16.toNat_sub_of_le (a b : UInt16) : b ≤ a → (a - b).toNat = a.toNat - b.toNat

@[simp]

theorem UInt16.toBitVec_max {a b : UInt16} : (max a b).toBitVec = max a.toBitVec b.toBitVec

theorem UInt16.add_def (a b : UInt16) : a + b = { toBitVec := a.toBitVec + b.toBitVec }

theorem UInt16.toBitVec_ne_of_ne {a b : UInt16} (h : a ≠ b) : a.toBitVec ≠ b.toBitVec

@[simp]

theorem UInt16.ofBitVec_ofNat (n : Nat) : { toBitVec := BitVec.ofNat 16 n } = OfNat.ofNat n

@[simp]

theorem UInt16.toFin_toBitVec (x : UInt16) : x.toBitVec.toFin = x.toFin

theorem UInt16.toFin_inj {a b : UInt16} : a.toFin = b.toFin ↔ a = b

@[simp]

theorem UInt16.toBitVec_ofNat (n : Nat) : (OfNat.ofNat n).toBitVec = BitVec.ofNat 16 n

@[simp]

theorem UInt16.toBitVec_div {a b : UInt16} : (a / b).toBitVec = a.toBitVec / b.toBitVec

theorem UInt16.le_antisymm {a b : UInt16} (h₁ : a ≤ b) (h₂ : b ≤ a) : a = b

@[simp]

theorem UInt16.toNat_ofNatLT {n : Nat} {h : n < size} : (ofNatLT n h).toNat = n

@[simp]

theorem UInt16.not_le {a b : UInt16} : ¬a ≤ b ↔ b < a

@[simp]

theorem UInt16.toNat_mod (a b : UInt16) : (a % b).toNat = a.toNat % b.toNat

theorem UInt16.min_def {a b : UInt16} : min a b = if a ≤ b then a else b

theorem UInt16.zero_def : 0 = { toBitVec := 0 }

theorem UInt16.ne_iff_toBitVec_ne {a b : UInt16} : a ≠ b ↔ a.toBitVec ≠ b.toBitVec

theorem UInt16.toNat_sub (a b : UInt16) : (a - b).toNat = (2 ^ 16 - b.toNat + a.toNat) % 2 ^ 16

@[simp]

theorem UInt32.toBitVec_sub {a b : UInt32} : (a - b).toBitVec = a.toBitVec - b.toBitVec

@[simp]

theorem UInt32.le_refl (a : UInt32) : a ≤ a

theorem UInt32.le_rfl {a : UInt32} : a ≤ a

theorem UInt32.toNat_ofNat_of_lt {n : Nat} (h : n < size) : toNat (OfNat.ofNat n) = n

@[simp]

theorem UInt32.toNat_zero : toNat 0 = 0

theorem UInt32.le_antisymm {a b : UInt32} (h₁ : a ≤ b) (h₂ : b ≤ a) : a = b

theorem UInt32.toNat_ofNat {n : Nat} : (OfNat.ofNat n).toNat = n % 2 ^ 32

instance UInt32.instIsLinearOrder : Std.IsLinearOrder UInt32

@[simp]

theorem UInt32.toBitVec_min {a b : UInt32} : (min a b).toBitVec = min a.toBitVec b.toBitVec

@[simp]

theorem UInt32.toNat_toUInt8 (x : UInt32) : x.toUInt8.toNat = x.toNat % 2 ^ 8

@[simp]

theorem UInt32.lt_irrefl (a : UInt32) : ¬a < a

theorem UInt32.ne_iff_toBitVec_ne {a b : UInt32} : a ≠ b ↔ a.toBitVec ≠ b.toBitVec

theorem UInt32.lt_asymm {a b : UInt32} : a < b → ¬b < a

theorem UInt32.toNat_ofNat_of_lt' {n : Nat} (h : n < size) : (ofNat n).toNat = n

@[simp]

theorem UInt32.toBitVec_mod {a b : UInt32} : (a % b).toBitVec = a.toBitVec % b.toBitVec

@[simp]

theorem UInt32.toFin_toBitVec (x : UInt32) : x.toBitVec.toFin = x.toFin

@[simp]

theorem UInt32.toNat_mul (a b : UInt32) : (a * b).toNat = a.toNat * b.toNat % 2 ^ 32

theorem UInt32.lt_iff_toNat_lt {a b : UInt32} : a < b ↔ a.toNat < b.toNat

theorem UInt32.eq_iff_toBitVec_eq {a b : UInt32} : a = b ↔ a.toBitVec = b.toBitVec

theorem UInt32.toBitVec_ne_of_ne {a b : UInt32} (h : a ≠ b) : a.toBitVec ≠ b.toBitVec

theorem UInt32.le_antisymm_iff {a b : UInt32} : a = b ↔ a ≤ b ∧ b ≤ a

@[simp]

theorem UInt32.toNat_add (a b : UInt32) : (a + b).toNat = (a.toNat + b.toNat) % 2 ^ 32

theorem UInt32.add_def (a b : UInt32) : a + b = { toBitVec := a.toBitVec + b.toBitVec }

theorem UInt32.ne_of_lt {a b : UInt32} (h : a < b) : a ≠ b

@[simp]

theorem UInt32.toNat_div (a b : UInt32) : (a / b).toNat = a.toNat / b.toNat

theorem UInt32.le_trans {a b c : UInt32} : a ≤ b → b ≤ c → a ≤ c

theorem UInt32.toBitVec_eq_of_eq {a b : UInt32} (h : a = b) : a.toBitVec = b.toBitVec

theorem UInt32.le_iff_toNat_le {a b : UInt32} : a ≤ b ↔ a.toNat ≤ b.toNat

theorem UInt32.toFin_inj {a b : UInt32} : a.toFin = b.toFin ↔ a = b

theorem UInt32.toNat_inj {a b : UInt32} : a.toNat = b.toNat ↔ a = b

@[simp]

theorem UInt32.toBitVec_mul {a b : UInt32} : (a * b).toBitVec = a.toBitVec * b.toBitVec

@[simp]

theorem UInt32.toNat_ofNat' {n : Nat} : (ofNat n).toNat = n % 2 ^ 32

@[simp]

theorem UInt32.ofNat_one : ofNat 1 = 1

@[simp]

theorem UInt32.not_lt {a b : UInt32} : ¬a < b ↔ b ≤ a

theorem UInt32.lt_trans {a b c : UInt32} : a < b → b < c → a < c

theorem UInt32.min_def {a b : UInt32} : min a b = if a ≤ b then a else b

theorem UInt32.one_def : 1 = { toBitVec := 1 }

@[simp]

theorem UInt32.toNat_ofNatLT {n : Nat} {h : n < size} : (ofNatLT n h).toNat = n

theorem UInt32.sub_def (a b : UInt32) : a - b = { toBitVec := a.toBitVec - b.toBitVec }

instance UInt32.instLawfulOrderLT : Std.LawfulOrderLT UInt32

theorem UInt32.toBitVec_inj {a b : UInt32} : a.toBitVec = b.toBitVec ↔ a = b

theorem UInt32.eq_of_toBitVec_eq {a b : UInt32} (h : a.toBitVec = b.toBitVec) : a = b

theorem UInt32.toBitVec_ofNat' (n : Nat) : (ofNat n).toBitVec = BitVec.ofNat 32 n

@[simp]

theorem UInt32.toNat_toUSize (x : UInt32) : x.toUSize.toNat = x.toNat

@[simp]

theorem UInt32.toFin_ofNat (n : Nat) : (OfNat.ofNat n).toFin = OfNat.ofNat n

@[simp]

theorem UInt32.toBitVec_neg {a : UInt32} : (-a).toBitVec = -a.toBitVec

@[simp]

theorem UInt32.toNat_toUInt16 (x : UInt32) : x.toUInt16.toNat = x.toNat % 2 ^ 16

theorem UInt32.le_total (a b : UInt32) : a ≤ b ∨ b ≤ a

@[simp]

theorem UInt32.ofNat_toNat {x : UInt32} : ofNat x.toNat = x

@[simp]

theorem UInt32.toBitVec_add {a b : UInt32} : (a + b).toBitVec = a.toBitVec + b.toBitVec

theorem UInt32.le_iff_toBitVec_le {a b : UInt32} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec

@[simp]

theorem UInt32.toNat_toBitVec (x : UInt32) : x.toBitVec.toNat = x.toNat

theorem UInt32.mod_lt (a : UInt32) {b : UInt32} : 0 < b → a % b < b

@[simp]

theorem UInt32.toBitVec_ofNat (n : Nat) : (OfNat.ofNat n).toBitVec = BitVec.ofNat 32 n

@[simp]

theorem UInt32.toBitVec_div {a b : UInt32} : (a / b).toBitVec = a.toBitVec / b.toBitVec

@[simp]

theorem UInt32.toNat_ofBitVec {a : BitVec 32} : { toBitVec := a }.toNat = a.toNat

@[simp]

theorem UInt32.toNat_mod (a b : UInt32) : (a % b).toNat = a.toNat % b.toNat

@[simp]

theorem UInt32.ofBitVec_ofNat (n : Nat) : { toBitVec := BitVec.ofNat 32 n } = OfNat.ofNat n

theorem UInt32.toNat_sub (a b : UInt32) : (a - b).toNat = (2 ^ 32 - b.toNat + a.toNat) % 2 ^ 32

theorem UInt32.zero_def : 0 = { toBitVec := 0 }

theorem UInt32.mod_def (a b : UInt32) : a % b = { toBitVec := a.toBitVec % b.toBitVec }

theorem UInt32.mul_def (a b : UInt32) : a * b = { toBitVec := a.toBitVec * b.toBitVec }

theorem UInt32.ne_of_toBitVec_ne {a b : UInt32} (h : a.toBitVec ≠ b.toBitVec) : a ≠ b

@[simp]

theorem UInt32.toFin_val (x : UInt32) : ↑x.toFin = x.toNat

@[simp]

theorem UInt32.toBitVec_max {a b : UInt32} : (max a b).toBitVec = max a.toBitVec b.toBitVec

theorem UInt32.lt_iff_toBitVec_lt {a b : UInt32} : a < b ↔ a.toBitVec < b.toBitVec

theorem UInt32.eq_of_toFin_eq {a b : UInt32} (h : a.toFin = b.toFin) : a = b

theorem UInt32.toNat_lt_size (a : UInt32) : a.toNat < size

theorem UInt32.toNat_mod_lt {m : Nat} (u : UInt32) : 0 < m → (u % ofNat m).toNat < m

theorem UInt32.max_def {a b : UInt32} : max a b = if a ≤ b then b else a

theorem UInt32.toNat.inj {a b : UInt32} : a.toNat = b.toNat → a = b

@[simp]

theorem UInt32.toNat_toUInt64 (x : UInt32) : x.toUInt64.toNat = x.toNat

@[simp]

theorem UInt32.ofBitVec_toBitVec (a : UInt32) : { toBitVec := a.toBitVec } = a

@[simp]

theorem UInt32.toNat_sub_of_le (a b : UInt32) : b ≤ a → (a - b).toNat = a.toNat - b.toNat

@[simp]

theorem UInt32.not_le {a b : UInt32} : ¬a ≤ b ↔ b < a

@[simp]

theorem UInt64.toNat_sub_of_le (a b : UInt64) : b ≤ a → (a - b).toNat = a.toNat - b.toNat

theorem UInt64.toNat_lt_size (a : UInt64) : a.toNat < size

@[simp]

theorem UInt64.toNat_mul (a b : UInt64) : (a * b).toNat = a.toNat * b.toNat % 2 ^ 64

theorem UInt64.le_rfl {a : UInt64} : a ≤ a

@[simp]

theorem UInt64.not_lt {a b : UInt64} : ¬a < b ↔ b ≤ a

theorem UInt64.toBitVec_ofNat' (n : Nat) : (ofNat n).toBitVec = BitVec.ofNat 64 n

@[simp]

theorem UInt64.toNat_div (a b : UInt64) : (a / b).toNat = a.toNat / b.toNat

@[simp]

theorem UInt64.toNat_toBitVec (x : UInt64) : x.toBitVec.toNat = x.toNat

theorem UInt64.toNat_ofNat_of_lt' {n : Nat} (h : n < size) : (ofNat n).toNat = n

theorem UInt64.add_def (a b : UInt64) : a + b = { toBitVec := a.toBitVec + b.toBitVec }

theorem UInt64.le_iff_toBitVec_le {a b : UInt64} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec

theorem UInt64.toNat_sub (a b : UInt64) : (a - b).toNat = (2 ^ 64 - b.toNat + a.toNat) % 2 ^ 64

@[simp]

theorem UInt64.toNat_toUInt16 (x : UInt64) : x.toUInt16.toNat = x.toNat % 2 ^ 16

theorem UInt64.toNat_ofNat_of_lt {n : Nat} (h : n < size) : toNat (OfNat.ofNat n) = n

theorem UInt64.max_def {a b : UInt64} : max a b = if a ≤ b then b else a

@[simp]

theorem UInt64.toFin_ofNat (n : Nat) : (OfNat.ofNat n).toFin = OfNat.ofNat n

theorem UInt64.lt_asymm {a b : UInt64} : a < b → ¬b < a

theorem UInt64.one_def : 1 = { toBitVec := 1 }

theorem UInt64.mod_def (a b : UInt64) : a % b = { toBitVec := a.toBitVec % b.toBitVec }

@[simp]

theorem UInt64.ofNat_one : ofNat 1 = 1

theorem UInt64.sub_def (a b : UInt64) : a - b = { toBitVec := a.toBitVec - b.toBitVec }

@[simp]

theorem UInt64.not_le {a b : UInt64} : ¬a ≤ b ↔ b < a

@[simp]

theorem UInt64.toNat_ofNatLT {n : Nat} {h : n < size} : (ofNatLT n h).toNat = n

@[simp]

theorem UInt64.toNat_ofNat' {n : Nat} : (ofNat n).toNat = n % 2 ^ 64

@[simp]

theorem UInt64.lt_irrefl (a : UInt64) : ¬a < a

@[simp]

theorem UInt64.toBitVec_ofNat (n : Nat) : (OfNat.ofNat n).toBitVec = BitVec.ofNat 64 n

@[simp]

theorem UInt64.toBitVec_mul {a b : UInt64} : (a * b).toBitVec = a.toBitVec * b.toBitVec

theorem UInt64.eq_of_toBitVec_eq {a b : UInt64} (h : a.toBitVec = b.toBitVec) : a = b

theorem UInt64.le_iff_toNat_le {a b : UInt64} : a ≤ b ↔ a.toNat ≤ b.toNat

@[simp]

theorem UInt64.toNat_toUInt32 (x : UInt64) : x.toUInt32.toNat = x.toNat % 2 ^ 32

theorem UInt64.toBitVec_eq_of_eq {a b : UInt64} (h : a = b) : a.toBitVec = b.toBitVec

@[simp]

theorem UInt64.toBitVec_mod {a b : UInt64} : (a % b).toBitVec = a.toBitVec % b.toBitVec

theorem UInt64.le_total (a b : UInt64) : a ≤ b ∨ b ≤ a

theorem UInt64.ne_of_lt {a b : UInt64} (h : a < b) : a ≠ b

@[simp]

theorem UInt64.toNat_ofBitVec {a : BitVec 64} : { toBitVec := a }.toNat = a.toNat

theorem UInt64.le_antisymm {a b : UInt64} (h₁ : a ≤ b) (h₂ : b ≤ a) : a = b

@[simp]

theorem UInt64.le_refl (a : UInt64) : a ≤ a

theorem UInt64.le_antisymm_iff {a b : UInt64} : a = b ↔ a ≤ b ∧ b ≤ a

theorem UInt64.mod_lt (a : UInt64) {b : UInt64} : 0 < b → a % b < b

theorem UInt64.toNat_inj {a b : UInt64} : a.toNat = b.toNat ↔ a = b

theorem UInt64.eq_of_toFin_eq {a b : UInt64} (h : a.toFin = b.toFin) : a = b

@[simp]

theorem UInt64.toFin_toBitVec (x : UInt64) : x.toBitVec.toFin = x.toFin

theorem UInt64.toFin_inj {a b : UInt64} : a.toFin = b.toFin ↔ a = b

@[simp]

theorem UInt64.toBitVec_min {a b : UInt64} : (min a b).toBitVec = min a.toBitVec b.toBitVec

@[simp]

theorem UInt64.ofBitVec_toBitVec (a : UInt64) : { toBitVec := a.toBitVec } = a

@[simp]

theorem UInt64.toBitVec_max {a b : UInt64} : (max a b).toBitVec = max a.toBitVec b.toBitVec

theorem UInt64.toBitVec_ne_of_ne {a b : UInt64} (h : a ≠ b) : a.toBitVec ≠ b.toBitVec

@[simp]

theorem UInt64.toBitVec_neg {a : UInt64} : (-a).toBitVec = -a.toBitVec

theorem UInt64.toNat_ofNat {n : Nat} : (OfNat.ofNat n).toNat = n % 2 ^ 64

theorem UInt64.lt_trans {a b c : UInt64} : a < b → b < c → a < c

@[simp]

theorem UInt64.toNat_toUSize (x : UInt64) : x.toUSize.toNat = x.toNat % 2 ^ System.Platform.numBits

theorem UInt64.toNat.inj {a b : UInt64} : a.toNat = b.toNat → a = b

@[simp]

theorem UInt64.toBitVec_sub {a b : UInt64} : (a - b).toBitVec = a.toBitVec - b.toBitVec

@[simp]

theorem UInt64.toNat_toUInt8 (x : UInt64) : x.toUInt8.toNat = x.toNat % 2 ^ 8

@[simp]

theorem UInt64.toNat_zero : toNat 0 = 0

@[simp]

theorem UInt64.ofBitVec_ofNat (n : Nat) : { toBitVec := BitVec.ofNat 64 n } = OfNat.ofNat n

theorem UInt64.lt_iff_toNat_lt {a b : UInt64} : a < b ↔ a.toNat < b.toNat

@[simp]

theorem UInt64.toBitVec_add {a b : UInt64} : (a + b).toBitVec = a.toBitVec + b.toBitVec

theorem UInt64.zero_def : 0 = { toBitVec := 0 }

theorem UInt64.toBitVec_inj {a b : UInt64} : a.toBitVec = b.toBitVec ↔ a = b

@[simp]

theorem UInt64.toNat_mod (a b : UInt64) : (a % b).toNat = a.toNat % b.toNat

theorem UInt64.toNat_mod_lt {m : Nat} (u : UInt64) : 0 < m → (u % ofNat m).toNat < m

instance UInt64.instIsLinearOrder : Std.IsLinearOrder UInt64

@[simp]

theorem UInt64.toNat_add (a b : UInt64) : (a + b).toNat = (a.toNat + b.toNat) % 2 ^ 64

theorem UInt64.le_trans {a b c : UInt64} : a ≤ b → b ≤ c → a ≤ c

theorem UInt64.mul_def (a b : UInt64) : a * b = { toBitVec := a.toBitVec * b.toBitVec }

theorem UInt64.lt_iff_toBitVec_lt {a b : UInt64} : a < b ↔ a.toBitVec < b.toBitVec

theorem UInt64.min_def {a b : UInt64} : min a b = if a ≤ b then a else b

@[simp]

theorem UInt64.ofNat_toNat {x : UInt64} : ofNat x.toNat = x

theorem UInt64.ne_iff_toBitVec_ne {a b : UInt64} : a ≠ b ↔ a.toBitVec ≠ b.toBitVec

theorem UInt64.eq_iff_toBitVec_eq {a b : UInt64} : a = b ↔ a.toBitVec = b.toBitVec

@[simp]

theorem UInt64.toFin_val (x : UInt64) : ↑x.toFin = x.toNat

@[simp]

theorem UInt64.toBitVec_div {a b : UInt64} : (a / b).toBitVec = a.toBitVec / b.toBitVec

theorem UInt64.ne_of_toBitVec_ne {a b : UInt64} (h : a.toBitVec ≠ b.toBitVec) : a ≠ b

instance UInt64.instLawfulOrderLT : Std.LawfulOrderLT UInt64

instance USize.instIsLinearOrder : Std.IsLinearOrder USize

@[simp]

theorem USize.toFin_val (x : USize) : ↑x.toFin = x.toNat

@[simp]

theorem USize.toFin_ofNat (n : Nat) : (OfNat.ofNat n).toFin = OfNat.ofNat n

@[simp]

theorem USize.toNat_toBitVec (x : USize) : x.toBitVec.toNat = x.toNat

theorem USize.le_trans {a b c : USize} : a ≤ b → b ≤ c → a ≤ c

theorem USize.toBitVec_ne_of_ne {a b : USize} (h : a ≠ b) : a.toBitVec ≠ b.toBitVec

@[simp]

theorem USize.toNat_add (a b : USize) : (a + b).toNat = (a.toNat + b.toNat) % 2 ^ System.Platform.numBits

@[simp]

theorem USize.toFin_toBitVec (x : USize) : x.toBitVec.toFin = x.toFin

@[simp]

theorem USize.toNat_mul (a b : USize) : (a * b).toNat = a.toNat * b.toNat % 2 ^ System.Platform.numBits

theorem USize.ne_iff_toBitVec_ne {a b : USize} : a ≠ b ↔ a.toBitVec ≠ b.toBitVec

@[simp]

theorem USize.ofBitVec_toBitVec (a : USize) : { toBitVec := a.toBitVec } = a

theorem USize.max_def {a b : USize} : max a b = if a ≤ b then b else a

@[simp]

theorem USize.toBitVec_ofNat (n : Nat) : (OfNat.ofNat n).toBitVec = BitVec.ofNat System.Platform.numBits n

theorem USize.sub_def (a b : USize) : a - b = { toBitVec := a.toBitVec - b.toBitVec }

@[simp]

theorem USize.toBitVec_mul {a b : USize} : (a * b).toBitVec = a.toBitVec * b.toBitVec

theorem USize.lt_asymm {a b : USize} : a < b → ¬b < a

@[simp]

theorem USize.lt_irrefl (a : USize) : ¬a < a

theorem USize.ne_of_toBitVec_ne {a b : USize} (h : a.toBitVec ≠ b.toBitVec) : a ≠ b

@[simp]

theorem USize.toNat_mod (a b : USize) : (a % b).toNat = a.toNat % b.toNat

theorem USize.toNat_ofNat_of_lt {n : Nat} (h : n < size) : toNat (OfNat.ofNat n) = n

@[simp]

theorem USize.not_lt {a b : USize} : ¬a < b ↔ b ≤ a

@[simp]

theorem USize.toBitVec_min {a b : USize} : (min a b).toBitVec = min a.toBitVec b.toBitVec

@[simp]

theorem USize.toNat_div (a b : USize) : (a / b).toNat = a.toNat / b.toNat

theorem USize.toBitVec_eq_of_eq {a b : USize} (h : a = b) : a.toBitVec = b.toBitVec

@[simp]

theorem USize.toNat_ofBitVec {a : BitVec System.Platform.numBits} : { toBitVec := a }.toNat = a.toNat

theorem USize.toNat_ofNat {n : Nat} : (OfNat.ofNat n).toNat = n % 2 ^ System.Platform.numBits

instance USize.instLawfulOrderLT : Std.LawfulOrderLT USize

@[simp]

theorem USize.toBitVec_max {a b : USize} : (max a b).toBitVec = max a.toBitVec b.toBitVec

theorem USize.eq_of_toBitVec_eq {a b : USize} (h : a.toBitVec = b.toBitVec) : a = b

@[simp]

theorem USize.toBitVec_sub {a b : USize} : (a - b).toBitVec = a.toBitVec - b.toBitVec

@[simp]

theorem USize.toNat_zero : toNat 0 = 0

theorem USize.lt_iff_toBitVec_lt {a b : USize} : a < b ↔ a.toBitVec < b.toBitVec

theorem USize.eq_of_toFin_eq {a b : USize} (h : a.toFin = b.toFin) : a = b

theorem USize.toNat_mod_lt {m : Nat} (u : USize) : 0 < m → (u % ofNat m).toNat < m

theorem USize.le_iff_toBitVec_le {a b : USize} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec

theorem USize.toNat_sub (a b : USize) : (a - b).toNat = (2 ^ System.Platform.numBits - b.toNat + a.toNat) % 2 ^ System.Platform.numBits

theorem USize.one_def : 1 = { toBitVec := 1 }

@[simp]

theorem USize.ofBitVec_ofNat (n : Nat) : { toBitVec := BitVec.ofNat System.Platform.numBits n } = OfNat.ofNat n

@[simp]

theorem USize.toBitVec_div {a b : USize} : (a / b).toBitVec = a.toBitVec / b.toBitVec

theorem USize.zero_def : 0 = { toBitVec := 0 }

@[simp]

theorem USize.toNat_ofNatLT {n : Nat} {h : n < size} : (ofNatLT n h).toNat = n

theorem USize.lt_trans {a b c : USize} : a < b → b < c → a < c

theorem USize.toBitVec_ofNat' (n : Nat) : (ofNat n).toBitVec = BitVec.ofNat System.Platform.numBits n

theorem USize.eq_iff_toBitVec_eq {a b : USize} : a = b ↔ a.toBitVec = b.toBitVec

theorem USize.add_def (a b : USize) : a + b = { toBitVec := a.toBitVec + b.toBitVec }

@[simp]

theorem USize.toBitVec_neg {a : USize} : (-a).toBitVec = -a.toBitVec

theorem USize.mod_lt (a : USize) {b : USize} : 0 < b → a % b < b

theorem USize.toNat_lt_size (a : USize) : a.toNat < size

theorem USize.ne_of_lt {a b : USize} (h : a < b) : a ≠ b

theorem USize.toNat_inj {a b : USize} : a.toNat = b.toNat ↔ a = b

@[simp]

theorem USize.le_refl (a : USize) : a ≤ a

theorem USize.le_total (a b : USize) : a ≤ b ∨ b ≤ a

theorem USize.mod_def (a b : USize) : a % b = { toBitVec := a.toBitVec % b.toBitVec }

theorem USize.le_iff_toNat_le {a b : USize} : a ≤ b ↔ a.toNat ≤ b.toNat

@[simp]

theorem USize.not_le {a b : USize} : ¬a ≤ b ↔ b < a

theorem USize.min_def {a b : USize} : min a b = if a ≤ b then a else b

theorem USize.le_antisymm {a b : USize} (h₁ : a ≤ b) (h₂ : b ≤ a) : a = b

theorem USize.toBitVec_inj {a b : USize} : a.toBitVec = b.toBitVec ↔ a = b

theorem USize.lt_iff_toNat_lt {a b : USize} : a < b ↔ a.toNat < b.toNat

theorem USize.le_antisymm_iff {a b : USize} : a = b ↔ a ≤ b ∧ b ≤ a

@[simp]

theorem USize.toBitVec_add {a b : USize} : (a + b).toBitVec = a.toBitVec + b.toBitVec

@[simp]

theorem USize.toNat_sub_of_le (a b : USize) : b ≤ a → (a - b).toNat = a.toNat - b.toNat

theorem USize.toNat.inj {a b : USize} : a.toNat = b.toNat → a = b

theorem USize.toNat_ofNat_of_lt' {n : Nat} (h : n < size) : (ofNat n).toNat = n

theorem USize.toFin_inj {a b : USize} : a.toFin = b.toFin ↔ a = b

theorem USize.le_rfl {a : USize} : a ≤ a

@[simp]

theorem USize.toNat_ofNat' {n : Nat} : (ofNat n).toNat = n % 2 ^ System.Platform.numBits

@[simp]

theorem USize.ofNat_toNat {x : USize} : ofNat x.toNat = x

@[simp]

theorem USize.ofNat_one : ofNat 1 = 1

@[simp]

theorem USize.toBitVec_mod {a b : USize} : (a % b).toBitVec = a.toBitVec % b.toBitVec

theorem USize.mul_def (a b : USize) : a * b = { toBitVec := a.toBitVec * b.toBitVec }

@[simp]

theorem USize.toNat_ofNat32 {n : Nat} {h : n < 4294967296} : (ofNat32 n h).toNat = n

@[simp]

theorem USize.toNat_toUInt8 (x : USize) : x.toUInt8.toNat = x.toNat % 2 ^ 8

@[simp]

theorem USize.toNat_toUInt16 (x : USize) : x.toUInt16.toNat = x.toNat % 2 ^ 16

@[simp]

theorem USize.toNat_toUInt32 (x : USize) : x.toUInt32.toNat = x.toNat % 2 ^ 32

@[simp]

theorem USize.toNat_toUInt64 (x : USize) : x.toUInt64.toNat = x.toNat

theorem USize.toNat_ofNat_of_lt_32 {n : Nat} (h : n < 4294967296) : (ofNat n).toNat = n

theorem UInt8.ofNat_mod_size {x : Nat} : ofNat (x % 2 ^ 8) = ofNat x

theorem UInt16.ofNat_mod_size {x : Nat} : ofNat (x % 2 ^ 16) = ofNat x

theorem UInt32.ofNat_mod_size {x : Nat} : ofNat (x % 2 ^ 32) = ofNat x

theorem UInt64.ofNat_mod_size {x : Nat} : ofNat (x % 2 ^ 64) = ofNat x

theorem USize.ofNat_mod_size {x : Nat} : ofNat (x % 2 ^ System.Platform.numBits) = ofNat x

theorem UInt8.ofNat_size : ofNat size = 0

theorem UInt16.ofNat_size : ofNat size = 0

theorem UInt32.ofNat_size : ofNat size = 0

theorem UInt64.ofNat_size : ofNat size = 0

theorem USize.ofNat_size : ofNat size = 0

theorem UInt8.lt_ofNat_iff {n : UInt8} {m : Nat} (h : m < size) : n < ofNat m ↔ n.toNat < m

theorem UInt8.ofNat_lt_iff {n : UInt8} {m : Nat} (h : m < size) : ofNat m < n ↔ m < n.toNat

theorem UInt8.le_ofNat_iff {n : UInt8} {m : Nat} (h : m < size) : n ≤ ofNat m ↔ n.toNat ≤ m

theorem UInt8.ofNat_le_iff {n : UInt8} {m : Nat} (h : m < size) : ofNat m ≤ n ↔ m ≤ n.toNat

theorem UInt16.lt_ofNat_iff {n : UInt16} {m : Nat} (h : m < size) : n < ofNat m ↔ n.toNat < m

theorem UInt16.ofNat_lt_iff {n : UInt16} {m : Nat} (h : m < size) : ofNat m < n ↔ m < n.toNat

theorem UInt16.le_ofNat_iff {n : UInt16} {m : Nat} (h : m < size) : n ≤ ofNat m ↔ n.toNat ≤ m

theorem UInt16.ofNat_le_iff {n : UInt16} {m : Nat} (h : m < size) : ofNat m ≤ n ↔ m ≤ n.toNat

theorem UInt32.lt_ofNat_iff {n : UInt32} {m : Nat} (h : m < size) : n < ofNat m ↔ n.toNat < m

theorem UInt32.ofNat_lt_iff {n : UInt32} {m : Nat} (h : m < size) : ofNat m < n ↔ m < n.toNat

theorem UInt32.le_ofNat_iff {n : UInt32} {m : Nat} (h : m < size) : n ≤ ofNat m ↔ n.toNat ≤ m

theorem UInt32.ofNat_le_iff {n : UInt32} {m : Nat} (h : m < size) : ofNat m ≤ n ↔ m ≤ n.toNat

theorem UInt64.lt_ofNat_iff {n : UInt64} {m : Nat} (h : m < size) : n < ofNat m ↔ n.toNat < m

theorem UInt64.ofNat_lt_iff {n : UInt64} {m : Nat} (h : m < size) : ofNat m < n ↔ m < n.toNat

theorem UInt64.le_ofNat_iff {n : UInt64} {m : Nat} (h : m < size) : n ≤ ofNat m ↔ n.toNat ≤ m

theorem UInt64.ofNat_le_iff {n : UInt64} {m : Nat} (h : m < size) : ofNat m ≤ n ↔ m ≤ n.toNat

theorem USize.lt_ofNat_iff {n : USize} {m : Nat} (h : m < size) : n < ofNat m ↔ n.toNat < m

theorem USize.ofNat_lt_iff {n : USize} {m : Nat} (h : m < size) : ofNat m < n ↔ m < n.toNat

theorem USize.le_ofNat_iff {n : USize} {m : Nat} (h : m < size) : n ≤ ofNat m ↔ n.toNat ≤ m

theorem USize.ofNat_le_iff {n : USize} {m : Nat} (h : m < size) : ofNat m ≤ n ↔ m ≤ n.toNat

theorem UInt8.mod_eq_of_lt {a b : UInt8} (h : a < b) : a % b = a

theorem UInt16.mod_eq_of_lt {a b : UInt16} (h : a < b) : a % b = a

theorem UInt32.mod_eq_of_lt {a b : UInt32} (h : a < b) : a % b = a

theorem UInt64.mod_eq_of_lt {a b : UInt64} (h : a < b) : a % b = a

theorem USize.mod_eq_of_lt {a b : USize} (h : a < b) : a % b = a

@[simp]

theorem UInt8.toNat_lt (n : UInt8) : n.toNat < 2 ^ 8

@[simp]

theorem UInt16.toNat_lt (n : UInt16) : n.toNat < 2 ^ 16

@[simp]

theorem UInt32.toNat_lt (n : UInt32) : n.toNat < 2 ^ 32

@[simp]

theorem UInt64.toNat_lt (n : UInt64) : n.toNat < 2 ^ 64

theorem UInt8.size_lt_usizeSize : size < USize.size

theorem UInt8.size_le_usizeSize : size ≤ USize.size

theorem UInt16.size_lt_usizeSize : size < USize.size

theorem UInt16.size_le_usizeSize : size ≤ USize.size

theorem UInt32.size_le_usizeSize : size ≤ USize.size

theorem USize.size_eq_two_pow : size = 2 ^ System.Platform.numBits

theorem USize.toNat_lt_two_pow_numBits (n : USize) : n.toNat < 2 ^ System.Platform.numBits

@[simp]

theorem USize.toNat_lt (n : USize) : n.toNat < 2 ^ 64

theorem USize.size_le_uint64Size : size ≤ UInt64.size

theorem UInt8.toNat_lt_usizeSize (n : UInt8) : n.toNat < USize.size

theorem UInt16.toNat_lt_usizeSize (n : UInt16) : n.toNat < USize.size

theorem UInt32.toNat_lt_usizeSize (n : UInt32) : n.toNat < USize.size

theorem UInt8.size_dvd_usizeSize : size ∣ USize.size

theorem UInt16.size_dvd_usizeSize : size ∣ USize.size

theorem UInt32.size_dvd_usizeSize : size ∣ USize.size

theorem USize.size_dvd_uInt64Size : size ∣ UInt64.size

@[simp]

theorem mod_usizeSize_uInt8Size (n : Nat) : n % USize.size % UInt8.size = n % UInt8.size

@[simp]

theorem mod_usizeSize_uInt16Size (n : Nat) : n % USize.size % UInt16.size = n % UInt16.size

@[simp]

theorem mod_usizeSize_uInt32Size (n : Nat) : n % USize.size % UInt32.size = n % UInt32.size

@[simp]

theorem mod_uInt64Size_uSizeSize (n : Nat) : n % UInt64.size % USize.size = n % USize.size

@[simp]

theorem USize.size_sub_one_mod_uint8Size : (size - 1) % UInt8.size = UInt8.size - 1

@[simp]

theorem USize.size_sub_one_mod_uint16Size : (size - 1) % UInt16.size = UInt16.size - 1

@[simp]

theorem USize.size_sub_one_mod_uint32Size : (size - 1) % UInt32.size = UInt32.size - 1

@[simp]

theorem UInt64.size_sub_one_mod_uSizeSize : 18446744073709551615 % USize.size = USize.size - 1

@[simp]

theorem UInt8.toNat_mod_size (n : UInt8) : n.toNat % size = n.toNat

@[simp]

theorem UInt8.toNat_mod_uInt16Size (n : UInt8) : n.toNat % UInt16.size = n.toNat

@[simp]

theorem UInt8.toNat_mod_uInt32Size (n : UInt8) : n.toNat % UInt32.size = n.toNat

@[simp]

theorem UInt8.toNat_mod_uInt64Size (n : UInt8) : n.toNat % UInt64.size = n.toNat

@[simp]

theorem UInt8.toNat_mod_uSizeSize (n : UInt8) : n.toNat % USize.size = n.toNat

@[simp]

theorem UInt16.toNat_mod_size (n : UInt16) : n.toNat % size = n.toNat

@[simp]

theorem UInt16.toNat_mod_uInt32Size (n : UInt16) : n.toNat % UInt32.size = n.toNat

@[simp]

theorem UInt16.toNat_mod_uInt64Size (n : UInt16) : n.toNat % UInt64.size = n.toNat

@[simp]

theorem UInt16.toNat_mod_uSizeSize (n : UInt16) : n.toNat % USize.size = n.toNat

@[simp]

theorem UInt32.toNat_mod_size (n : UInt32) : n.toNat % size = n.toNat

@[simp]

theorem UInt32.toNat_mod_uInt64Size (n : UInt32) : n.toNat % UInt64.size = n.toNat

@[simp]

theorem UInt32.toNat_mod_uSizeSize (n : UInt32) : n.toNat % USize.size = n.toNat

@[simp]

theorem UInt64.toNat_mod_size (n : UInt64) : n.toNat % size = n.toNat

@[simp]

theorem USize.toNat_mod_size (n : USize) : n.toNat % size = n.toNat

@[simp]

theorem USize.toNat_mod_uInt64Size (n : USize) : n.toNat % UInt64.size = n.toNat

@[simp]

theorem UInt8.toUInt16_mod_256 (n : UInt8) : n.toUInt16 % 256 = n.toUInt16

@[simp]

theorem UInt8.toUInt32_mod_256 (n : UInt8) : n.toUInt32 % 256 = n.toUInt32

@[simp]

theorem UInt8.toUInt64_mod_256 (n : UInt8) : n.toUInt64 % 256 = n.toUInt64

@[simp]

theorem UInt8.toUSize_mod_256 (n : UInt8) : n.toUSize % 256 = n.toUSize

@[simp]

theorem UInt16.toUInt32_mod_65536 (n : UInt16) : n.toUInt32 % 65536 = n.toUInt32

@[simp]

theorem UInt16.toUInt64_mod_65536 (n : UInt16) : n.toUInt64 % 65536 = n.toUInt64

@[simp]

theorem UInt16.toUSize_mod_65536 (n : UInt16) : n.toUSize % 65536 = n.toUSize

@[simp]

theorem UInt32.toUInt64_mod_4294967296 (n : UInt32) : n.toUInt64 % 4294967296 = n.toUInt64

@[simp]

theorem Fin.mk_uInt8ToNat (n : UInt8) : ⟨n.toNat, ⋯⟩ = n.toFin

@[simp]

theorem Fin.mk_uInt16ToNat (n : UInt16) : ⟨n.toNat, ⋯⟩ = n.toFin

@[simp]

theorem Fin.mk_uInt32ToNat (n : UInt32) : ⟨n.toNat, ⋯⟩ = n.toFin

@[simp]

theorem Fin.mk_uInt64ToNat (n : UInt64) : ⟨n.toNat, ⋯⟩ = n.toFin

@[simp]

theorem Fin.mk_uSizeToNat (n : USize) : ⟨n.toNat, ⋯⟩ = n.toFin

@[simp]

theorem BitVec.ofNatLT_uInt8ToNat (n : UInt8) : n.toNat#'⋯ = n.toBitVec

@[simp]

theorem BitVec.ofNatLT_uInt16ToNat (n : UInt16) : n.toNat#'⋯ = n.toBitVec

@[simp]

theorem BitVec.ofNatLT_uInt32ToNat (n : UInt32) : n.toNat#'⋯ = n.toBitVec

@[simp]

theorem BitVec.ofNatLT_uInt64ToNat (n : UInt64) : n.toNat#'⋯ = n.toBitVec

@[simp]

theorem BitVec.ofNatLT_uSizeToNat (n : USize) : n.toNat#'⋯ = n.toBitVec

@[simp]

theorem BitVec.ofFin_uInt8ToFin (n : UInt8) : { toFin := n.toFin } = n.toBitVec

@[simp]

theorem BitVec.ofFin_uInt16ToFin (n : UInt16) : { toFin := n.toFin } = n.toBitVec

@[simp]

theorem BitVec.ofFin_uInt32ToFin (n : UInt32) : { toFin := n.toFin } = n.toBitVec

@[simp]

theorem BitVec.ofFin_uInt64ToFin (n : UInt64) : { toFin := n.toFin } = n.toBitVec

@[simp]

theorem BitVec.ofFin_uSizeToFin (n : USize) : { toFin := n.toFin } = n.toBitVec

@[simp]

theorem UInt8.toFin_toUInt16 (n : UInt8) : n.toUInt16.toFin = Fin.castLE toFin_toUInt16._proof_1 n.toFin

@[simp]

theorem UInt8.toFin_toUInt32 (n : UInt8) : n.toUInt32.toFin = Fin.castLE toFin_toUInt32._proof_1 n.toFin

@[simp]

theorem UInt8.toFin_toUInt64 (n : UInt8) : n.toUInt64.toFin = Fin.castLE toFin_toUInt64._proof_1 n.toFin

@[simp]

theorem UInt8.toFin_toUSize (n : UInt8) : n.toUSize.toFin = Fin.castLE size_le_usizeSize n.toFin

@[simp]

theorem UInt16.toFin_toUInt32 (n : UInt16) : n.toUInt32.toFin = Fin.castLE toFin_toUInt32._proof_1 n.toFin

@[simp]

theorem UInt16.toFin_toUInt64 (n : UInt16) : n.toUInt64.toFin = Fin.castLE toFin_toUInt64._proof_1 n.toFin

@[simp]

theorem UInt16.toFin_toUSize (n : UInt16) : n.toUSize.toFin = Fin.castLE size_le_usizeSize n.toFin

@[simp]

theorem UInt32.toFin_toUInt64 (n : UInt32) : n.toUInt64.toFin = Fin.castLE toFin_toUInt64._proof_1 n.toFin

@[simp]

theorem UInt32.toFin_toUSize (n : UInt32) : n.toUSize.toFin = Fin.castLE size_le_usizeSize n.toFin

@[simp]

theorem USize.toFin_toUInt64 (n : USize) : n.toUInt64.toFin = Fin.castLE size_le_uint64Size n.toFin

@[simp]

theorem UInt16.toBitVec_toUInt8 (n : UInt16) : n.toUInt8.toBitVec = BitVec.setWidth 8 n.toBitVec

@[simp]

theorem UInt32.toBitVec_toUInt8 (n : UInt32) : n.toUInt8.toBitVec = BitVec.setWidth 8 n.toBitVec

@[simp]

theorem UInt64.toBitVec_toUInt8 (n : UInt64) : n.toUInt8.toBitVec = BitVec.setWidth 8 n.toBitVec

@[simp]

theorem USize.toBitVec_toUInt8 (n : USize) : n.toUInt8.toBitVec = BitVec.setWidth 8 n.toBitVec

@[simp]

theorem UInt8.toBitVec_toUInt16 (n : UInt8) : n.toUInt16.toBitVec = BitVec.setWidth 16 n.toBitVec

@[simp]

theorem UInt32.toBitVec_toUInt16 (n : UInt32) : n.toUInt16.toBitVec = BitVec.setWidth 16 n.toBitVec

@[simp]

theorem UInt64.toBitVec_toUInt16 (n : UInt64) : n.toUInt16.toBitVec = BitVec.setWidth 16 n.toBitVec

@[simp]

theorem USize.toBitVec_toUInt16 (n : USize) : n.toUInt16.toBitVec = BitVec.setWidth 16 n.toBitVec

@[simp]

theorem UInt8.toBitVec_toUInt32 (n : UInt8) : n.toUInt32.toBitVec = BitVec.setWidth 32 n.toBitVec

@[simp]

theorem UInt16.toBitVec_toUInt32 (n : UInt16) : n.toUInt32.toBitVec = BitVec.setWidth 32 n.toBitVec

@[simp]

theorem UInt64.toBitVec_toUInt32 (n : UInt64) : n.toUInt32.toBitVec = BitVec.setWidth 32 n.toBitVec

@[simp]

theorem USize.toBitVec_toUInt32 (n : USize) : n.toUInt32.toBitVec = BitVec.setWidth 32 n.toBitVec

@[simp]

theorem UInt8.toBitVec_toUInt64 (n : UInt8) : n.toUInt64.toBitVec = BitVec.setWidth 64 n.toBitVec

@[simp]

theorem UInt16.toBitVec_toUInt64 (n : UInt16) : n.toUInt64.toBitVec = BitVec.setWidth 64 n.toBitVec

@[simp]

theorem UInt32.toBitVec_toUInt64 (n : UInt32) : n.toUInt64.toBitVec = BitVec.setWidth 64 n.toBitVec

@[simp]

theorem USize.toBitVec_toUInt64 (n : USize) : n.toUInt64.toBitVec = BitVec.setWidth 64 n.toBitVec

@[simp]

theorem UInt8.toBitVec_toUSize (n : UInt8) : n.toUSize.toBitVec = BitVec.setWidth System.Platform.numBits n.toBitVec

@[simp]

theorem UInt16.toBitVec_toUSize (n : UInt16) : n.toUSize.toBitVec = BitVec.setWidth System.Platform.numBits n.toBitVec

@[simp]

theorem UInt32.toBitVec_toUSize (n : UInt32) : n.toUSize.toBitVec = BitVec.setWidth System.Platform.numBits n.toBitVec

@[simp]

theorem UInt64.toBitVec_toUSize (n : UInt64) : n.toUSize.toBitVec = BitVec.setWidth System.Platform.numBits n.toBitVec

@[simp]

theorem UInt8.ofNatLT_toNat (n : UInt8) : ofNatLT n.toNat ⋯ = n

@[simp]

theorem UInt16.ofNatLT_uInt8ToNat (n : UInt8) : ofNatLT n.toNat ⋯ = n.toUInt16

@[simp]

theorem UInt32.ofNatLT_uInt8ToNat (n : UInt8) : ofNatLT n.toNat ⋯ = n.toUInt32

@[simp]

theorem UInt64.ofNatLT_uInt8ToNat (n : UInt8) : ofNatLT n.toNat ⋯ = n.toUInt64

@[simp]

theorem USize.ofNatLT_uInt8ToNat (n : UInt8) : ofNatLT n.toNat ⋯ = n.toUSize

@[simp]

theorem UInt16.ofNatLT_toNat (n : UInt16) : ofNatLT n.toNat ⋯ = n

@[simp]

theorem UInt32.ofNatLT_uInt16ToNat (n : UInt16) : ofNatLT n.toNat ⋯ = n.toUInt32

@[simp]

theorem UInt64.ofNatLT_uInt16ToNat (n : UInt16) : ofNatLT n.toNat ⋯ = n.toUInt64

@[simp]

theorem USize.ofNatLT_uInt16ToNat (n : UInt16) : ofNatLT n.toNat ⋯ = n.toUSize

@[simp]

theorem UInt32.ofNatLT_toNat (n : UInt32) : ofNatLT n.toNat ⋯ = n

@[simp]

theorem UInt64.ofNatLT_uInt32ToNat (n : UInt32) : ofNatLT n.toNat ⋯ = n.toUInt64

@[simp]

theorem USize.ofNatLT_uInt32ToNat (n : UInt32) : ofNatLT n.toNat ⋯ = n.toUSize

@[simp]

theorem UInt64.ofNatLT_toNat (n : UInt64) : ofNatLT n.toNat ⋯ = n

@[simp]

theorem USize.ofNatLT_toNat (n : USize) : ofNatLT n.toNat ⋯ = n

@[simp]

theorem UInt64.ofNatLT_uSizeToNat (n : USize) : ofNatLT n.toNat ⋯ = n.toUInt64

theorem UInt8.ofNatLT_uInt16ToNat (n : UInt16) (h : n.toNat < size) : ofNatLT n.toNat h = n.toUInt8

theorem UInt8.ofNatLT_uInt32ToNat (n : UInt32) (h : n.toNat < size) : ofNatLT n.toNat h = n.toUInt8

theorem UInt8.ofNatLT_uInt64ToNat (n : UInt64) (h : n.toNat < size) : ofNatLT n.toNat h = n.toUInt8

theorem UInt8.ofNatLT_uSizeToNat (n : USize) (h : n.toNat < size) : ofNatLT n.toNat h = n.toUInt8

theorem UInt16.ofNatLT_uInt32ToNat (n : UInt32) (h : n.toNat < size) : ofNatLT n.toNat h = n.toUInt16

theorem UInt16.ofNatLT_uInt64ToNat (n : UInt64) (h : n.toNat < size) : ofNatLT n.toNat h = n.toUInt16

theorem UInt16.ofNatLT_uSizeToNat (n : USize) (h : n.toNat < size) : ofNatLT n.toNat h = n.toUInt16

theorem UInt32.ofNatLT_uInt64ToNat (n : UInt64) (h : n.toNat < size) : ofNatLT n.toNat h = n.toUInt32

theorem UInt32.ofNatLT_uSizeToNat (n : USize) (h : n.toNat < size) : ofNatLT n.toNat h = n.toUInt32

theorem USize.ofNatLT_uInt64ToNat (n : UInt64) (h : n.toNat < size) : ofNatLT n.toNat h = n.toUSize

@[simp]

theorem UInt8.ofFin_toFin (n : UInt8) : ofFin n.toFin = n

@[simp]

theorem UInt16.ofFin_toFin (n : UInt16) : ofFin n.toFin = n

@[simp]

theorem UInt32.ofFin_toFin (n : UInt32) : ofFin n.toFin = n

@[simp]

theorem UInt64.ofFin_toFin (n : UInt64) : ofFin n.toFin = n

@[simp]

theorem USize.ofFin_toFin (n : USize) : ofFin n.toFin = n

@[simp]

theorem UInt8.toFin_ofFin (n : Fin size) : (ofFin n).toFin = n

@[simp]

theorem UInt16.toFin_ofFin (n : Fin size) : (ofFin n).toFin = n

@[simp]

theorem UInt32.toFin_ofFin (n : Fin size) : (ofFin n).toFin = n

@[simp]

theorem UInt64.toFin_ofFin (n : Fin size) : (ofFin n).toFin = n

@[simp]

theorem USize.toFin_ofFin (n : Fin size) : (ofFin n).toFin = n

@[simp]

theorem UInt16.ofFin_uint8ToFin (n : UInt8) : ofFin (Fin.castLE UInt8.toFin_toUInt16._proof_1 n.toFin) = n.toUInt16

@[simp]

theorem UInt32.ofFin_uint8ToFin (n : UInt8) : ofFin (Fin.castLE UInt8.toFin_toUInt32._proof_1 n.toFin) = n.toUInt32

@[simp]

theorem UInt32.ofFin_uint16ToFin (n : UInt16) : ofFin (Fin.castLE UInt16.toFin_toUInt32._proof_1 n.toFin) = n.toUInt32

@[simp]

theorem UInt64.ofFin_uint8ToFin (n : UInt8) : ofFin (Fin.castLE UInt8.toFin_toUInt64._proof_1 n.toFin) = n.toUInt64

@[simp]

theorem UInt64.ofFin_uint16ToFin (n : UInt16) : ofFin (Fin.castLE UInt16.toFin_toUInt64._proof_1 n.toFin) = n.toUInt64

@[simp]

theorem UInt64.ofFin_uint32ToFin (n : UInt32) : ofFin (Fin.castLE UInt32.toFin_toUInt64._proof_1 n.toFin) = n.toUInt64

@[simp]

theorem USize.ofFin_uint8ToFin (n : UInt8) : ofFin (Fin.castLE UInt8.size_le_usizeSize n.toFin) = n.toUSize

@[simp]

theorem USize.ofFin_uint16ToFin (n : UInt16) : ofFin (Fin.castLE UInt16.size_le_usizeSize n.toFin) = n.toUSize

@[simp]

theorem USize.ofFin_uint32ToFin (n : UInt32) : ofFin (Fin.castLE UInt32.size_le_usizeSize n.toFin) = n.toUSize

@[simp]

theorem Nat.toUInt8_eq {n : Nat} : n.toUInt8 = UInt8.ofNat n

@[simp]

theorem Nat.toUInt16_eq {n : Nat} : n.toUInt16 = UInt16.ofNat n

@[simp]

theorem Nat.toUInt32_eq {n : Nat} : n.toUInt32 = UInt32.ofNat n

@[simp]

theorem Nat.toUInt64_eq {n : Nat} : n.toUInt64 = UInt64.ofNat n

@[simp]

theorem Nat.toUSize_eq {n : Nat} : n.toUSize = USize.ofNat n

@[simp]

theorem UInt8.ofBitVec_uInt16ToBitVec (n : UInt16) : { toBitVec := BitVec.setWidth 8 n.toBitVec } = n.toUInt8

@[simp]

theorem UInt8.ofBitVec_uInt32ToBitVec (n : UInt32) : { toBitVec := BitVec.setWidth 8 n.toBitVec } = n.toUInt8

@[simp]

theorem UInt8.ofBitVec_uInt64ToBitVec (n : UInt64) : { toBitVec := BitVec.setWidth 8 n.toBitVec } = n.toUInt8

@[simp]

theorem UInt8.ofBitVec_uSizeToBitVec (n : USize) : { toBitVec := BitVec.setWidth 8 n.toBitVec } = n.toUInt8

@[simp]

theorem UInt16.ofBitVec_uInt8ToBitVec (n : UInt8) : { toBitVec := BitVec.setWidth 16 n.toBitVec } = n.toUInt16

@[simp]

theorem UInt16.ofBitVec_uInt32ToBitVec (n : UInt32) : { toBitVec := BitVec.setWidth 16 n.toBitVec } = n.toUInt16

@[simp]

theorem UInt16.ofBitVec_uInt64ToBitVec (n : UInt64) : { toBitVec := BitVec.setWidth 16 n.toBitVec } = n.toUInt16

@[simp]

theorem UInt16.ofBitVec_uSizeToBitVec (n : USize) : { toBitVec := BitVec.setWidth 16 n.toBitVec } = n.toUInt16

@[simp]

theorem UInt32.ofBitVec_uInt8ToBitVec (n : UInt8) : { toBitVec := BitVec.setWidth 32 n.toBitVec } = n.toUInt32

@[simp]

theorem UInt32.ofBitVec_uInt16ToBitVec (n : UInt16) : { toBitVec := BitVec.setWidth 32 n.toBitVec } = n.toUInt32

@[simp]

theorem UInt32.ofBitVec_uInt64ToBitVec (n : UInt64) : { toBitVec := BitVec.setWidth 32 n.toBitVec } = n.toUInt32

@[simp]

theorem UInt32.ofBitVec_uSizeToBitVec (n : USize) : { toBitVec := BitVec.setWidth 32 n.toBitVec } = n.toUInt32

@[simp]

theorem UInt64.ofBitVec_uInt8ToBitVec (n : UInt8) : { toBitVec := BitVec.setWidth 64 n.toBitVec } = n.toUInt64

@[simp]

theorem UInt64.ofBitVec_uInt16ToBitVec (n : UInt16) : { toBitVec := BitVec.setWidth 64 n.toBitVec } = n.toUInt64

@[simp]

theorem UInt64.ofBitVec_uInt32ToBitVec (n : UInt32) : { toBitVec := BitVec.setWidth 64 n.toBitVec } = n.toUInt64

@[simp]

theorem UInt64.ofBitVec_uSizeToBitVec (n : USize) : { toBitVec := BitVec.setWidth 64 n.toBitVec } = n.toUInt64

@[simp]

theorem USize.ofBitVec_uInt8ToBitVec (n : UInt8) : { toBitVec := BitVec.setWidth System.Platform.numBits n.toBitVec } = n.toUSize

@[simp]

theorem USize.ofBitVec_uInt16ToBitVec (n : UInt16) : { toBitVec := BitVec.setWidth System.Platform.numBits n.toBitVec } = n.toUSize

@[simp]

theorem USize.ofBitVec_uInt32ToBitVec (n : UInt32) : { toBitVec := BitVec.setWidth System.Platform.numBits n.toBitVec } = n.toUSize

@[simp]

theorem USize.ofBitVec_uInt64ToBitVec (n : UInt64) : { toBitVec := BitVec.setWidth System.Platform.numBits n.toBitVec } = n.toUSize

@[simp]

theorem UInt8.ofNat_uInt16ToNat (n : UInt16) : ofNat n.toNat = n.toUInt8

@[simp]

theorem UInt8.ofNat_uInt32ToNat (n : UInt32) : ofNat n.toNat = n.toUInt8

@[simp]

theorem UInt8.ofNat_uInt64ToNat (n : UInt64) : ofNat n.toNat = n.toUInt8

@[simp]

theorem UInt8.ofNat_uSizeToNat (n : USize) : ofNat n.toNat = n.toUInt8

@[simp]

theorem UInt16.ofNat_uInt8ToNat (n : UInt8) : ofNat n.toNat = n.toUInt16

@[simp]

theorem UInt16.ofNat_uInt32ToNat (n : UInt32) : ofNat n.toNat = n.toUInt16

@[simp]

theorem UInt16.ofNat_uInt64ToNat (n : UInt64) : ofNat n.toNat = n.toUInt16

@[simp]

theorem UInt16.ofNat_uSizeToNat (n : USize) : ofNat n.toNat = n.toUInt16

@[simp]

theorem UInt32.ofNat_uInt8ToNat (n : UInt8) : ofNat n.toNat = n.toUInt32

@[simp]

theorem UInt32.ofNat_uInt16ToNat (n : UInt16) : ofNat n.toNat = n.toUInt32

@[simp]

theorem UInt32.ofNat_uInt64ToNat (n : UInt64) : ofNat n.toNat = n.toUInt32

@[simp]

theorem UInt32.ofNat_uSizeToNat (n : USize) : ofNat n.toNat = n.toUInt32

@[simp]

theorem UInt64.ofNat_uInt8ToNat (n : UInt8) : ofNat n.toNat = n.toUInt64

@[simp]

theorem UInt64.ofNat_uInt16ToNat (n : UInt16) : ofNat n.toNat = n.toUInt64

@[simp]

theorem UInt64.ofNat_uInt32ToNat (n : UInt32) : ofNat n.toNat = n.toUInt64

@[simp]

theorem UInt64.ofNat_uSizeToNat (n : USize) : ofNat n.toNat = n.toUInt64

@[simp]

theorem USize.ofNat_uInt8ToNat (n : UInt8) : ofNat n.toNat = n.toUSize

@[simp]

theorem USize.ofNat_uInt16ToNat (n : UInt16) : ofNat n.toNat = n.toUSize

@[simp]

theorem USize.ofNat_uInt32ToNat (n : UInt32) : ofNat n.toNat = n.toUSize

@[simp]

theorem USize.ofNat_uInt64ToNat (n : UInt64) : ofNat n.toNat = n.toUSize

theorem UInt8.ofNatLT_eq_ofNat (n : Nat) {h : n < size} : ofNatLT n h = ofNat n

theorem UInt16.ofNatLT_eq_ofNat (n : Nat) {h : n < size} : ofNatLT n h = ofNat n

theorem UInt32.ofNatLT_eq_ofNat (n : Nat) {h : n < size} : ofNatLT n h = ofNat n

theorem UInt64.ofNatLT_eq_ofNat (n : Nat) {h : n < size} : ofNatLT n h = ofNat n

theorem USize.ofNatLT_eq_ofNat (n : Nat) {h : n < size} : ofNatLT n h = ofNat n

theorem UInt8.ofNatClamp_eq_ofNat (n : Nat) (hn : n < size) : ofNatClamp n = ofNat n

theorem UInt16.ofNatClamp_eq_ofNat (n : Nat) (hn : n < size) : ofNatClamp n = ofNat n

theorem UInt32.ofNatClamp_eq_ofNat (n : Nat) (hn : n < size) : ofNatClamp n = ofNat n

theorem UInt64.ofNatClamp_eq_ofNat (n : Nat) (hn : n < size) : ofNatClamp n = ofNat n

theorem USize.ofNatClamp_eq_ofNat (n : Nat) (hn : n < size) : ofNatClamp n = ofNat n

@[simp]

theorem UInt8.ofNatClamp_toNat (n : UInt8) : ofNatClamp n.toNat = n

@[simp]

theorem UInt16.ofNatClamp_uInt8ToNat (n : UInt8) : ofNatClamp n.toNat = n.toUInt16

@[simp]

theorem UInt16.ofNatClamp_toNat (n : UInt16) : ofNatClamp n.toNat = n

@[simp]

theorem UInt32.ofNatClamp_uInt8ToNat (n : UInt8) : ofNatClamp n.toNat = n.toUInt32

@[simp]

theorem UInt32.ofNatClamp_uInt16ToNat (n : UInt16) : ofNatClamp n.toNat = n.toUInt32

@[simp]

theorem UInt32.ofNatClamp_toNat (n : UInt32) : ofNatClamp n.toNat = n

@[simp]

theorem UInt64.ofNatClamp_uInt8ToNat (n : UInt8) : ofNatClamp n.toNat = n.toUInt64

@[simp]

theorem UInt64.ofNatClamp_uInt16ToNat (n : UInt16) : ofNatClamp n.toNat = n.toUInt64

@[simp]

theorem UInt64.ofNatClamp_uInt32ToNat (n : UInt32) : ofNatClamp n.toNat = n.toUInt64

@[simp]

theorem UInt64.ofNatClamp_toNat (n : UInt64) : ofNatClamp n.toNat = n

@[simp]

theorem UInt64.ofNatClamp_uSizeToNat (n : USize) : ofNatClamp n.toNat = n.toUInt64

@[simp]

theorem USize.ofNatClamp_uInt8ToNat (n : UInt8) : ofNatClamp n.toNat = n.toUSize

@[simp]

theorem USize.ofNatClamp_uInt16ToNat (n : UInt16) : ofNatClamp n.toNat = n.toUSize

@[simp]

theorem USize.ofNatClamp_uInt32ToNat (n : UInt32) : ofNatClamp n.toNat = n.toUSize

@[simp]

theorem USize.ofNatClamp_toNat (n : USize) : ofNatClamp n.toNat = n

@[simp]

theorem UInt8.toUInt8_toUInt16 (n : UInt8) : n.toUInt16.toUInt8 = n

@[simp]

theorem UInt8.toUInt8_toUInt32 (n : UInt8) : n.toUInt32.toUInt8 = n

@[simp]

theorem UInt8.toUInt8_toUInt64 (n : UInt8) : n.toUInt64.toUInt8 = n

@[simp]

theorem UInt8.toUInt8_toUSize (n : UInt8) : n.toUSize.toUInt8 = n

@[simp]

theorem UInt8.toUInt16_toUInt32 (n : UInt8) : n.toUInt32.toUInt16 = n.toUInt16

@[simp]

theorem UInt8.toUInt16_toUInt64 (n : UInt8) : n.toUInt64.toUInt16 = n.toUInt16

@[simp]

theorem UInt8.toUInt16_toUSize (n : UInt8) : n.toUSize.toUInt16 = n.toUInt16

@[simp]

theorem UInt8.toUInt32_toUInt16 (n : UInt8) : n.toUInt16.toUInt32 = n.toUInt32

@[simp]

theorem UInt8.toUInt32_toUInt64 (n : UInt8) : n.toUInt64.toUInt32 = n.toUInt32

@[simp]

theorem UInt8.toUInt32_toUSize (n : UInt8) : n.toUSize.toUInt32 = n.toUInt32

@[simp]

theorem UInt8.toUInt64_toUInt16 (n : UInt8) : n.toUInt16.toUInt64 = n.toUInt64

@[simp]

theorem UInt8.toUInt64_toUInt32 (n : UInt8) : n.toUInt32.toUInt64 = n.toUInt64

@[simp]

theorem UInt8.toUInt64_toUSize (n : UInt8) : n.toUSize.toUInt64 = n.toUInt64

@[simp]

theorem UInt8.toUSize_toUInt16 (n : UInt8) : n.toUInt16.toUSize = n.toUSize

@[simp]

theorem UInt8.toUSize_toUInt32 (n : UInt8) : n.toUInt32.toUSize = n.toUSize

@[simp]

theorem UInt8.toUSize_toUInt64 (n : UInt8) : n.toUInt64.toUSize = n.toUSize

@[simp]

theorem UInt16.toUInt8_toUInt32 (n : UInt16) : n.toUInt32.toUInt8 = n.toUInt8

@[simp]

theorem UInt16.toUInt8_toUInt64 (n : UInt16) : n.toUInt64.toUInt8 = n.toUInt8

@[simp]

theorem UInt16.toUInt8_toUSize (n : UInt16) : n.toUSize.toUInt8 = n.toUInt8

@[simp]

theorem UInt16.toUInt16_toUInt8 (n : UInt16) : n.toUInt8.toUInt16 = n % 256

@[simp]

theorem UInt16.toUInt16_toUInt32 (n : UInt16) : n.toUInt32.toUInt16 = n

@[simp]

theorem UInt16.toUInt16_toUInt64 (n : UInt16) : n.toUInt64.toUInt16 = n

@[simp]

theorem UInt16.toUInt16_toUSize (n : UInt16) : n.toUSize.toUInt16 = n

@[simp]

theorem UInt16.toUInt32_toUInt8 (n : UInt16) : n.toUInt8.toUInt32 = n.toUInt32 % 256

@[simp]

theorem UInt16.toUInt32_toUInt64 (n : UInt16) : n.toUInt64.toUInt32 = n.toUInt32

@[simp]

theorem UInt16.toUInt32_toUSize (n : UInt16) : n.toUSize.toUInt32 = n.toUInt32

@[simp]

theorem UInt16.toUInt64_toUInt8 (n : UInt16) : n.toUInt8.toUInt64 = n.toUInt64 % 256

@[simp]

theorem UInt16.toUInt64_toUInt32 (n : UInt16) : n.toUInt32.toUInt64 = n.toUInt64

@[simp]

theorem UInt16.toUInt64_toUSize (n : UInt16) : n.toUSize.toUInt64 = n.toUInt64

@[simp]

theorem UInt16.toUSize_toUInt8 (n : UInt16) : n.toUInt8.toUSize = n.toUSize % 256

@[simp]

theorem UInt16.toUSize_toUInt32 (n : UInt16) : n.toUInt32.toUSize = n.toUSize

@[simp]

theorem UInt16.toUSize_toUInt64 (n : UInt16) : n.toUInt64.toUSize = n.toUSize

@[simp]

theorem UInt32.toUInt8_toUInt16 (n : UInt32) : n.toUInt16.toUInt8 = n.toUInt8

@[simp]

theorem UInt32.toUInt8_toUInt64 (n : UInt32) : n.toUInt64.toUInt8 = n.toUInt8

@[simp]

theorem UInt32.toUInt8_toUSize (n : UInt32) : n.toUSize.toUInt8 = n.toUInt8

@[simp]

theorem UInt32.toUInt16_toUInt8 (n : UInt32) : n.toUInt8.toUInt16 = n.toUInt16 % 256

@[simp]

theorem UInt32.toUInt16_toUInt64 (n : UInt32) : n.toUInt64.toUInt16 = n.toUInt16

@[simp]

theorem UInt32.toUInt16_toUSize (n : UInt32) : n.toUSize.toUInt16 = n.toUInt16

@[simp]

theorem UInt32.toUInt32_toUInt8 (n : UInt32) : n.toUInt8.toUInt32 = n % 256

@[simp]

theorem UInt32.toUInt32_toUInt16 (n : UInt32) : n.toUInt16.toUInt32 = n % 65536

@[simp]

theorem UInt32.toUInt32_toUInt64 (n : UInt32) : n.toUInt64.toUInt32 = n

@[simp]

theorem UInt32.toUInt32_toUSize (n : UInt32) : n.toUSize.toUInt32 = n

@[simp]

theorem UInt32.toUInt64_toUInt8 (n : UInt32) : n.toUInt8.toUInt64 = n.toUInt64 % 256

@[simp]

theorem UInt32.toUInt64_toUInt16 (n : UInt32) : n.toUInt16.toUInt64 = n.toUInt64 % 65536

@[simp]

theorem UInt32.toUInt64_toUSize (n : UInt32) : n.toUSize.toUInt64 = n.toUInt64

@[simp]

theorem UInt32.toUSize_toUInt8 (n : UInt32) : n.toUInt8.toUSize = n.toUSize % 256

@[simp]

theorem UInt32.toUSize_toUInt16 (n : UInt32) : n.toUInt16.toUSize = n.toUSize % 65536

@[simp]

theorem UInt32.toUSize_toUInt64 (n : UInt32) : n.toUInt64.toUSize = n.toUSize

@[simp]

theorem UInt64.toUInt8_toUInt16 (n : UInt64) : n.toUInt16.toUInt8 = n.toUInt8

@[simp]

theorem UInt64.toUInt8_toUInt32 (n : UInt64) : n.toUInt32.toUInt8 = n.toUInt8

@[simp]

theorem UInt64.toUInt8_toUSize (n : UInt64) : n.toUSize.toUInt8 = n.toUInt8

@[simp]

theorem UInt64.toUInt16_toUInt8 (n : UInt64) : n.toUInt8.toUInt16 = n.toUInt16 % 256

@[simp]

theorem UInt64.toUInt16_toUInt32 (n : UInt64) : n.toUInt32.toUInt16 = n.toUInt16

@[simp]

theorem UInt64.toUInt16_toUSize (n : UInt64) : n.toUSize.toUInt16 = n.toUInt16

@[simp]

theorem UInt64.toUInt32_toUInt8 (n : UInt64) : n.toUInt8.toUInt32 = n.toUInt32 % 256

@[simp]

theorem UInt64.toUInt32_toUInt16 (n : UInt64) : n.toUInt16.toUInt32 = n.toUInt32 % 65536

@[simp]

theorem UInt64.toUInt32_toUSize (n : UInt64) : n.toUSize.toUInt32 = n.toUInt32

@[simp]

theorem UInt64.toUInt64_toUInt8 (n : UInt64) : n.toUInt8.toUInt64 = n % 256

@[simp]

theorem UInt64.toUInt64_toUInt16 (n : UInt64) : n.toUInt16.toUInt64 = n % 65536

@[simp]

theorem UInt64.toUInt64_toUInt32 (n : UInt64) : n.toUInt32.toUInt64 = n % 4294967296

@[simp]

theorem UInt64.toUSize_toUInt8 (n : UInt64) : n.toUInt8.toUSize = n.toUSize % 256

@[simp]

theorem UInt64.toUSize_toUInt16 (n : UInt64) : n.toUInt16.toUSize = n.toUSize % 65536

@[simp]

theorem USize.toUInt8_toUInt16 (n : USize) : n.toUInt16.toUInt8 = n.toUInt8

@[simp]

theorem USize.toUInt8_toUInt32 (n : USize) : n.toUInt32.toUInt8 = n.toUInt8

@[simp]

theorem USize.toUInt8_toUInt64 (n : USize) : n.toUInt64.toUInt8 = n.toUInt8

@[simp]

theorem USize.toUInt16_toUInt8 (n : USize) : n.toUInt8.toUInt16 = n.toUInt16 % 256

@[simp]

theorem USize.toUInt16_toUInt32 (n : USize) : n.toUInt32.toUInt16 = n.toUInt16

@[simp]

theorem USize.toUInt16_toUInt64 (n : USize) : n.toUInt64.toUInt16 = n.toUInt16

@[simp]

theorem USize.toUInt64_toUInt8 (n : USize) : n.toUInt8.toUInt64 = n.toUInt64 % 256

@[simp]

theorem USize.toUInt64_toUInt16 (n : USize) : n.toUInt16.toUInt64 = n.toUInt64 % 65536

@[simp]

theorem USize.toUInt32_toUInt8 (n : USize) : n.toUInt8.toUInt32 = n.toUInt32 % 256

@[simp]

theorem USize.toUInt32_toUInt16 (n : USize) : n.toUInt16.toUInt32 = n.toUInt32 % 65536

@[simp]

theorem USize.toUInt32_toUInt64 (n : USize) : n.toUInt64.toUInt32 = n.toUInt32

@[simp]

theorem USize.toUSize_toUInt8 (n : USize) : n.toUInt8.toUSize = n % 256

@[simp]

theorem USize.toUSize_toUInt16 (n : USize) : n.toUInt16.toUSize = n % 65536

@[simp]

theorem USize.toUSize_toUInt64 (n : USize) : n.toUInt64.toUSize = n

@[simp]

theorem USize.toUSize_toUInt32 (n : USize) : n.toUInt32.toUSize = n % 4294967296

@[simp]

theorem UInt8.toNat_ofFin (x : Fin size) : (ofFin x).toNat = ↑x

@[simp]

theorem UInt16.toNat_ofFin (x : Fin size) : (ofFin x).toNat = ↑x

@[simp]

theorem UInt32.toNat_ofFin (x : Fin size) : (ofFin x).toNat = ↑x

@[simp]

theorem UInt64.toNat_ofFin (x : Fin size) : (ofFin x).toNat = ↑x

@[simp]

theorem USize.toNat_ofFin (x : Fin size) : (ofFin x).toNat = ↑x

theorem UInt8.toNat_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toNat = n

theorem UInt16.toNat_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toNat = n

theorem UInt32.toNat_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toNat = n

theorem UInt64.toNat_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toNat = n

theorem USize.toNat_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toNat = n

theorem UInt8.toNat_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toNat = size - 1

theorem UInt16.toNat_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toNat = size - 1

theorem UInt32.toNat_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toNat = size - 1

theorem UInt64.toNat_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toNat = size - 1

theorem USize.toNat_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toNat = size - 1

@[simp]

theorem UInt8.toFin_ofNatLT {n : Nat} (hn : n < size) : (ofNatLT n hn).toFin = ⟨n, hn⟩

@[simp]

theorem UInt16.toFin_ofNatLT {n : Nat} (hn : n < size) : (ofNatLT n hn).toFin = ⟨n, hn⟩

@[simp]

theorem UInt32.toFin_ofNatLT {n : Nat} (hn : n < size) : (ofNatLT n hn).toFin = ⟨n, hn⟩

@[simp]

theorem UInt64.toFin_ofNatLT {n : Nat} (hn : n < size) : (ofNatLT n hn).toFin = ⟨n, hn⟩

@[simp]

theorem USize.toFin_ofNatLT {n : Nat} (hn : n < size) : (ofNatLT n hn).toFin = ⟨n, hn⟩

@[simp]

theorem UInt8.toFin.ofNat {n : Nat} : (UInt8.ofNat n).toFin = Fin.ofNat size n

@[simp]

theorem UInt16.toFin.ofNat {n : Nat} : (UInt16.ofNat n).toFin = Fin.ofNat size n

@[simp]

theorem UInt32.toFin.ofNat {n : Nat} : (UInt32.ofNat n).toFin = Fin.ofNat size n

@[simp]

theorem UInt64.toFin.ofNat {n : Nat} : (UInt64.ofNat n).toFin = Fin.ofNat size n

@[simp]

theorem USize.toFin.ofNat {n : Nat} : (USize.ofNat n).toFin = Fin.ofNat size n

@[simp]

theorem UInt8.toFin_ofBitVec {b : BitVec 8} : { toBitVec := b }.toFin = b.toFin

@[simp]

theorem UInt16.toFin_ofBitVec {b : BitVec 16} : { toBitVec := b }.toFin = b.toFin

@[simp]

theorem UInt32.toFin_ofBitVec {b : BitVec 32} : { toBitVec := b }.toFin = b.toFin

@[simp]

theorem UInt64.toFin_ofBitVec {b : BitVec 64} : { toBitVec := b }.toFin = b.toFin

@[simp]

theorem USize.toFin_ofBitVec {b : BitVec System.Platform.numBits} : { toBitVec := b }.toFin = b.toFin

theorem UInt8.toFin_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toFin = ⟨n, hn⟩

theorem UInt16.toFin_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toFin = ⟨n, hn⟩

theorem UInt32.toFin_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toFin = ⟨n, hn⟩

theorem UInt64.toFin_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toFin = ⟨n, hn⟩

theorem USize.toFin_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toFin = ⟨n, hn⟩

theorem UInt8.toFin_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toFin = ⟨size - 1, toFin_ofNatClamp_of_le._proof_1⟩

theorem UInt16.toFin_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toFin = ⟨size - 1, toFin_ofNatClamp_of_le._proof_1⟩

theorem UInt32.toFin_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toFin = ⟨size - 1, toFin_ofNatClamp_of_le._proof_1⟩

theorem UInt64.toFin_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toFin = ⟨size - 1, toFin_ofNatClamp_of_le._proof_1⟩

theorem USize.toFin_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toFin = ⟨size - 1, toFin_ofNatClamp_of_le._proof_1⟩

@[simp]

theorem UInt8.toBitVec_ofNatLT {n : Nat} (hn : n < size) : (ofNatLT n hn).toBitVec = n#'hn

@[simp]

theorem UInt16.toBitVec_ofNatLT {n : Nat} (hn : n < size) : (ofNatLT n hn).toBitVec = n#'hn

@[simp]

theorem UInt32.toBitVec_ofNatLT {n : Nat} (hn : n < size) : (ofNatLT n hn).toBitVec = n#'hn

@[simp]

theorem UInt64.toBitVec_ofNatLT {n : Nat} (hn : n < size) : (ofNatLT n hn).toBitVec = n#'hn

@[simp]

theorem USize.toBitVec_ofNatLT {n : Nat} (hn : n < size) : (ofNatLT n hn).toBitVec = n#'hn

@[simp]

theorem UInt8.toBitVec_ofFin (n : Fin size) : (ofFin n).toBitVec = { toFin := n }

@[simp]

theorem UInt16.toBitVec_ofFin (n : Fin size) : (ofFin n).toBitVec = { toFin := n }

@[simp]

theorem UInt32.toBitVec_ofFin (n : Fin size) : (ofFin n).toBitVec = { toFin := n }

@[simp]

theorem UInt64.toBitVec_ofFin (n : Fin size) : (ofFin n).toBitVec = { toFin := n }

@[simp]

theorem USize.toBitVec_ofFin (n : Fin size) : (ofFin n).toBitVec = { toFin := n }

@[simp]

theorem UInt8.toBitVec_ofBitVec (n : BitVec 8) : { toBitVec := n }.toBitVec = n

@[simp]

theorem UInt16.toBitVec_ofBitVec (n : BitVec 16) : { toBitVec := n }.toBitVec = n

@[simp]

theorem UInt32.toBitVec_ofBitVec (n : BitVec 32) : { toBitVec := n }.toBitVec = n

@[simp]

theorem UInt64.toBitVec_ofBitVec (n : BitVec 64) : { toBitVec := n }.toBitVec = n

@[simp]

theorem USize.toBitVec_ofBitVec (n : BitVec System.Platform.numBits) : { toBitVec := n }.toBitVec = n

theorem UInt8.toBitVec_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toBitVec = n#'hn

theorem UInt16.toBitVec_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toBitVec = n#'hn

theorem UInt32.toBitVec_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toBitVec = n#'hn

theorem UInt64.toBitVec_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toBitVec = n#'hn

theorem USize.toBitVec_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toBitVec = n#'hn

theorem UInt8.toBitVec_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toBitVec = (size - 1)#'toBitVec_ofNatClamp_of_le._proof_1

theorem UInt16.toBitVec_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toBitVec = (size - 1)#'toBitVec_ofNatClamp_of_le._proof_1

theorem UInt32.toBitVec_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toBitVec = (size - 1)#'toBitVec_ofNatClamp_of_le._proof_1

theorem UInt64.toBitVec_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toBitVec = (size - 1)#'toBitVec_ofNatClamp_of_le._proof_1

theorem USize.toBitVec_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toBitVec = (size - 1)#'toBitVec_ofNatClamp_of_le._proof_1

@[simp]

theorem UInt16.toUInt8_ofNatLT {n : Nat} (hn : n < size) : (ofNatLT n hn).toUInt8 = UInt8.ofNat n

@[simp]

theorem UInt32.toUInt8_ofNatLT {n : Nat} (hn : n < size) : (ofNatLT n hn).toUInt8 = UInt8.ofNat n

@[simp]

theorem UInt64.toUInt8_ofNatLT {n : Nat} (hn : n < size) : (ofNatLT n hn).toUInt8 = UInt8.ofNat n

@[simp]

theorem USize.toUInt8_ofNatLT {n : Nat} (hn : n < size) : (ofNatLT n hn).toUInt8 = UInt8.ofNat n

@[simp]

theorem UInt16.toUInt8_ofFin (n : Fin size) : (ofFin n).toUInt8 = UInt8.ofNat ↑n

@[simp]

theorem UInt32.toUInt8_ofFin (n : Fin size) : (ofFin n).toUInt8 = UInt8.ofNat ↑n

@[simp]

theorem UInt64.toUInt8_ofFin (n : Fin size) : (ofFin n).toUInt8 = UInt8.ofNat ↑n

@[simp]

theorem USize.toUInt8_ofFin (n : Fin size) : (ofFin n).toUInt8 = UInt8.ofNat ↑n

@[simp]

theorem UInt16.toUInt8_ofBitVec (b : BitVec 16) : { toBitVec := b }.toUInt8 = { toBitVec := BitVec.setWidth 8 b }

@[simp]

theorem UInt32.toUInt8_ofBitVec (b : BitVec 32) : { toBitVec := b }.toUInt8 = { toBitVec := BitVec.setWidth 8 b }

@[simp]

theorem UInt64.toUInt8_ofBitVec (b : BitVec 64) : { toBitVec := b }.toUInt8 = { toBitVec := BitVec.setWidth 8 b }

@[simp]

theorem USize.toUInt8_ofBitVec (b : BitVec System.Platform.numBits) : { toBitVec := b }.toUInt8 = { toBitVec := BitVec.setWidth 8 b }

@[simp]

theorem UInt16.toUInt8_ofNat' (n : Nat) : (ofNat n).toUInt8 = UInt8.ofNat n

@[simp]

theorem UInt32.toUInt8_ofNat' (n : Nat) : (ofNat n).toUInt8 = UInt8.ofNat n

@[simp]

theorem UInt64.toUInt8_ofNat' (n : Nat) : (ofNat n).toUInt8 = UInt8.ofNat n

@[simp]

theorem USize.toUInt8_ofNat' (n : Nat) : (ofNat n).toUInt8 = UInt8.ofNat n

@[simp]

theorem UInt16.toUInt8_ofNat {n : Nat} : (OfNat.ofNat n).toUInt8 = OfNat.ofNat n

@[simp]

theorem UInt32.toUInt8_ofNat {n : Nat} : (OfNat.ofNat n).toUInt8 = OfNat.ofNat n

@[simp]

theorem UInt64.toUInt8_ofNat {n : Nat} : (OfNat.ofNat n).toUInt8 = OfNat.ofNat n

@[simp]

theorem USize.toUInt8_ofNat {n : Nat} : (OfNat.ofNat n).toUInt8 = OfNat.ofNat n

theorem UInt16.toUInt8_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt8 = UInt8.ofNat n

theorem UInt32.toUInt8_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt8 = UInt8.ofNat n

theorem UInt64.toUInt8_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt8 = UInt8.ofNat n

theorem USize.toUInt8_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt8 = UInt8.ofNat n

theorem UInt16.toUInt8_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt8 = UInt8.ofNatLT (UInt8.size - 1) toUInt8_ofNatClamp_of_le._proof_1

theorem UInt32.toUInt8_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt8 = UInt8.ofNatLT (UInt8.size - 1) UInt16.toUInt8_ofNatClamp_of_le._proof_1

theorem UInt64.toUInt8_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt8 = UInt8.ofNatLT (UInt8.size - 1) UInt16.toUInt8_ofNatClamp_of_le._proof_1

theorem USize.toUInt8_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt8 = UInt8.ofNatLT (UInt8.size - 1) UInt16.toUInt8_ofNatClamp_of_le._proof_1

@[simp]

theorem UInt32.toUInt16_ofNatLT {n : Nat} (hn : n < size) : (ofNatLT n hn).toUInt16 = UInt16.ofNat n

@[simp]

theorem UInt64.toUInt16_ofNatLT {n : Nat} (hn : n < size) : (ofNatLT n hn).toUInt16 = UInt16.ofNat n

@[simp]

theorem USize.toUInt16_ofNatLT {n : Nat} (hn : n < size) : (ofNatLT n hn).toUInt16 = UInt16.ofNat n

@[simp]

theorem UInt32.toUInt16_ofFin (n : Fin size) : (ofFin n).toUInt16 = UInt16.ofNat ↑n

@[simp]

theorem UInt64.toUInt16_ofFin (n : Fin size) : (ofFin n).toUInt16 = UInt16.ofNat ↑n

@[simp]

theorem USize.toUInt16_ofFin (n : Fin size) : (ofFin n).toUInt16 = UInt16.ofNat ↑n

@[simp]

theorem UInt32.toUInt16_ofBitVec (b : BitVec 32) : { toBitVec := b }.toUInt16 = { toBitVec := BitVec.setWidth 16 b }

@[simp]

theorem UInt64.toUInt16_ofBitVec (b : BitVec 64) : { toBitVec := b }.toUInt16 = { toBitVec := BitVec.setWidth 16 b }

@[simp]

theorem USize.toUInt16_ofBitVec (b : BitVec System.Platform.numBits) : { toBitVec := b }.toUInt16 = { toBitVec := BitVec.setWidth 16 b }

@[simp]

theorem UInt32.toUInt16_ofNat' (n : Nat) : (ofNat n).toUInt16 = UInt16.ofNat n

@[simp]

theorem UInt64.toUInt16_ofNat' (n : Nat) : (ofNat n).toUInt16 = UInt16.ofNat n

@[simp]

theorem USize.toUInt16_ofNat' (n : Nat) : (ofNat n).toUInt16 = UInt16.ofNat n

@[simp]

theorem UInt32.toUInt16_ofNat {n : Nat} : (OfNat.ofNat n).toUInt16 = OfNat.ofNat n

@[simp]

theorem UInt64.toUInt16_ofNat {n : Nat} : (OfNat.ofNat n).toUInt16 = OfNat.ofNat n

@[simp]

theorem USize.toUInt16_ofNat {n : Nat} : (OfNat.ofNat n).toUInt16 = OfNat.ofNat n

theorem UInt32.toUInt16_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt16 = UInt16.ofNat n

theorem UInt64.toUInt16_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt16 = UInt16.ofNat n

theorem USize.toUInt16_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt16 = UInt16.ofNat n

theorem UInt32.toUInt16_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt16 = UInt16.ofNatLT (UInt16.size - 1) toUInt16_ofNatClamp_of_le._proof_1

theorem UInt64.toUInt16_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt16 = UInt16.ofNatLT (UInt16.size - 1) UInt32.toUInt16_ofNatClamp_of_le._proof_1

theorem USize.toUInt16_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt16 = UInt16.ofNatLT (UInt16.size - 1) UInt32.toUInt16_ofNatClamp_of_le._proof_1

@[simp]

theorem UInt64.toUInt32_ofNatLT {n : Nat} (hn : n < size) : (ofNatLT n hn).toUInt32 = UInt32.ofNat n

@[simp]

theorem USize.toUInt32_ofNatLT {n : Nat} (hn : n < size) : (ofNatLT n hn).toUInt32 = UInt32.ofNat n

@[simp]

theorem UInt64.toUInt32_ofFin (n : Fin size) : (ofFin n).toUInt32 = UInt32.ofNat ↑n

@[simp]

theorem USize.toUInt32_ofFin (n : Fin size) : (ofFin n).toUInt32 = UInt32.ofNat ↑n

@[simp]

theorem UInt64.toUInt32_ofBitVec (b : BitVec 64) : { toBitVec := b }.toUInt32 = { toBitVec := BitVec.setWidth 32 b }

@[simp]

theorem USize.toUInt32_ofBitVec (b : BitVec System.Platform.numBits) : { toBitVec := b }.toUInt32 = { toBitVec := BitVec.setWidth 32 b }

@[simp]

theorem UInt64.toUInt32_ofNat' (n : Nat) : (ofNat n).toUInt32 = UInt32.ofNat n

@[simp]

theorem USize.toUInt32_ofNat' (n : Nat) : (ofNat n).toUInt32 = UInt32.ofNat n

@[simp]

theorem UInt64.toUInt32_ofNat {n : Nat} : (OfNat.ofNat n).toUInt32 = OfNat.ofNat n

@[simp]

theorem USize.toUInt32_ofNat {n : Nat} : (OfNat.ofNat n).toUInt32 = OfNat.ofNat n

theorem UInt64.toUInt32_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt32 = UInt32.ofNat n

theorem USize.toUInt32_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt32 = UInt32.ofNat n

theorem UInt64.toUInt32_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt32 = UInt32.ofNatLT (UInt32.size - 1) toUInt32_ofNatClamp_of_le._proof_1

theorem USize.toUInt32_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt32 = UInt32.ofNatLT (UInt32.size - 1) UInt64.toUInt32_ofNatClamp_of_le._proof_1

@[simp]

theorem UInt64.toUSize_ofNatLT {n : Nat} (hn : n < size) : (ofNatLT n hn).toUSize = USize.ofNat n

@[simp]

theorem UInt64.toUSize_ofFin (n : Fin size) : (ofFin n).toUSize = USize.ofNat ↑n

@[simp]

theorem UInt64.toUSize_ofBitVec (b : BitVec 64) : { toBitVec := b }.toUSize = { toBitVec := BitVec.setWidth System.Platform.numBits b }

@[simp]

theorem UInt64.toUSize_ofNat' (n : Nat) : (ofNat n).toUSize = USize.ofNat n

@[simp]

theorem UInt64.toUSize_ofNat {n : Nat} : (OfNat.ofNat n).toUSize = OfNat.ofNat n

theorem UInt64.toUSize_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUSize = USize.ofNat n

theorem UInt64.toUSize_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUSize = USize.ofNatLT (USize.size - 1) toUSize_ofNatClamp_of_le._proof_1

theorem UInt8.toUInt16_ofNatLT {n : Nat} (h : n < size) : (ofNatLT n h).toUInt16 = UInt16.ofNatLT n ⋯

theorem UInt8.toUInt32_ofNatLT {n : Nat} (h : n < size) : (ofNatLT n h).toUInt32 = UInt32.ofNatLT n ⋯

theorem UInt8.toUInt64_ofNatLT {n : Nat} (h : n < size) : (ofNatLT n h).toUInt64 = UInt64.ofNatLT n ⋯

theorem UInt8.toUSize_ofNatLT {n : Nat} (h : n < size) : (ofNatLT n h).toUSize = USize.ofNatLT n ⋯

theorem UInt8.toUInt16_ofFin {n : Fin size} : (ofFin n).toUInt16 = UInt16.ofNatLT ↑n ⋯

theorem UInt8.toUInt32_ofFin {n : Fin size} : (ofFin n).toUInt32 = UInt32.ofNatLT ↑n ⋯

theorem UInt8.toUInt64_ofFin {n : Fin size} : (ofFin n).toUInt64 = UInt64.ofNatLT ↑n ⋯

theorem UInt8.toUSize_ofFin {n : Fin size} : (ofFin n).toUSize = USize.ofNatLT ↑n ⋯

@[simp]

theorem UInt8.toUInt16_ofBitVec {b : BitVec 8} : { toBitVec := b }.toUInt16 = { toBitVec := BitVec.setWidth 16 b }

@[simp]

theorem UInt8.toUInt32_ofBitVec {b : BitVec 8} : { toBitVec := b }.toUInt32 = { toBitVec := BitVec.setWidth 32 b }

@[simp]

theorem UInt8.toUInt64_ofBitVec {b : BitVec 8} : { toBitVec := b }.toUInt64 = { toBitVec := BitVec.setWidth 64 b }

@[simp]

theorem UInt8.toUSize_ofBitVec {b : BitVec 8} : { toBitVec := b }.toUSize = { toBitVec := BitVec.setWidth System.Platform.numBits b }

theorem UInt8.toUInt16_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt16 = UInt16.ofNatLT n ⋯

theorem UInt8.toUInt32_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt32 = UInt32.ofNatLT n ⋯

theorem UInt8.toUInt64_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt64 = UInt64.ofNatLT n ⋯

theorem UInt8.toUSize_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUSize = USize.ofNatLT n ⋯

theorem UInt8.toUInt16_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt16 = UInt16.ofNatLT (size - 1) toUInt16_ofNatClamp_of_le._proof_1

theorem UInt8.toUInt32_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt32 = UInt32.ofNatLT (size - 1) toUInt32_ofNatClamp_of_le._proof_1

theorem UInt8.toUInt64_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt64 = UInt64.ofNatLT (size - 1) toUInt64_ofNatClamp_of_le._proof_1

theorem UInt8.toUSize_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUSize = USize.ofNatLT (size - 1) ⋯

theorem UInt16.toUInt32_ofNatLT {n : Nat} (h : n < size) : (ofNatLT n h).toUInt32 = UInt32.ofNatLT n ⋯

theorem UInt16.toUInt64_ofNatLT {n : Nat} (h : n < size) : (ofNatLT n h).toUInt64 = UInt64.ofNatLT n ⋯

theorem UInt16.toUSize_ofNatLT {n : Nat} (h : n < size) : (ofNatLT n h).toUSize = USize.ofNatLT n ⋯

theorem UInt16.toUInt32_ofFin {n : Fin size} : (ofFin n).toUInt32 = UInt32.ofNatLT ↑n ⋯

theorem UInt16.toUInt64_ofFin {n : Fin size} : (ofFin n).toUInt64 = UInt64.ofNatLT ↑n ⋯

theorem UInt16.toUSize_ofFin {n : Fin size} : (ofFin n).toUSize = USize.ofNatLT ↑n ⋯

@[simp]

theorem UInt16.toUInt32_ofBitVec {b : BitVec 16} : { toBitVec := b }.toUInt32 = { toBitVec := BitVec.setWidth 32 b }

@[simp]

theorem UInt16.toUInt64_ofBitVec {b : BitVec 16} : { toBitVec := b }.toUInt64 = { toBitVec := BitVec.setWidth 64 b }

@[simp]

theorem UInt16.toUSize_ofBitVec {b : BitVec 16} : { toBitVec := b }.toUSize = { toBitVec := BitVec.setWidth System.Platform.numBits b }

theorem UInt16.toUInt32_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt32 = UInt32.ofNatLT n ⋯

theorem UInt16.toUInt64_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt64 = UInt64.ofNatLT n ⋯

theorem UInt16.toUSize_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUSize = USize.ofNatLT n ⋯

theorem UInt16.toUInt32_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt32 = UInt32.ofNatLT (size - 1) toUInt32_ofNatClamp_of_le._proof_1

theorem UInt16.toUInt64_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt64 = UInt64.ofNatLT (size - 1) toUInt64_ofNatClamp_of_le._proof_1

theorem UInt16.toUSize_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUSize = USize.ofNatLT (size - 1) ⋯

theorem UInt32.toUInt64_ofNatLT {n : Nat} (h : n < size) : (ofNatLT n h).toUInt64 = UInt64.ofNatLT n ⋯

theorem UInt32.toUSize_ofNatLT {n : Nat} (h : n < size) : (ofNatLT n h).toUSize = USize.ofNatLT n ⋯

theorem UInt32.toUInt64_ofFin {n : Fin size} : (ofFin n).toUInt64 = UInt64.ofNatLT ↑n ⋯

theorem UInt32.toUSize_ofFin {n : Fin size} : (ofFin n).toUSize = USize.ofNatLT ↑n ⋯

@[simp]

theorem UInt32.toUInt64_ofBitVec {b : BitVec 32} : { toBitVec := b }.toUInt64 = { toBitVec := BitVec.setWidth 64 b }

@[simp]

theorem UInt32.toUSize_ofBitVec {b : BitVec 32} : { toBitVec := b }.toUSize = { toBitVec := BitVec.setWidth System.Platform.numBits b }

theorem UInt32.toUInt64_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt64 = UInt64.ofNatLT n ⋯

theorem UInt32.toUSize_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUSize = USize.ofNatLT n ⋯

theorem UInt32.toUInt64_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt64 = UInt64.ofNatLT (size - 1) toUInt64_ofNatClamp_of_le._proof_1

theorem UInt32.toUSize_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUSize = USize.ofNatLT (size - 1) ⋯

theorem USize.toUInt64_ofNatLT {n : Nat} (h : n < size) : (ofNatLT n h).toUInt64 = UInt64.ofNatLT n ⋯

theorem USize.toUInt64_ofFin {n : Fin size} : (ofFin n).toUInt64 = UInt64.ofNatLT ↑n ⋯

@[simp]

theorem USize.toUInt64_ofBitVec {b : BitVec System.Platform.numBits} : { toBitVec := b }.toUInt64 = { toBitVec := BitVec.setWidth 64 b }

theorem USize.toUInt64_ofNatClamp_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt64 = UInt64.ofNatLT n ⋯

theorem USize.toUInt64_ofNatClamp_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt64 = UInt64.ofNatLT (size - 1) toUInt64_ofNatClamp_of_le._proof_1

@[simp]

theorem UInt8.toUInt16_ofNat' {n : Nat} (hn : n < size) : (ofNat n).toUInt16 = UInt16.ofNat n

@[simp]

theorem UInt8.toUInt32_ofNat' {n : Nat} (hn : n < size) : (ofNat n).toUInt32 = UInt32.ofNat n

@[simp]

theorem UInt8.toUInt64_ofNat' {n : Nat} (hn : n < size) : (ofNat n).toUInt64 = UInt64.ofNat n

@[simp]

theorem UInt8.toUSize_ofNat' {n : Nat} (hn : n < size) : (ofNat n).toUSize = USize.ofNat n

@[simp]

theorem UInt16.toUInt32_ofNat' {n : Nat} (hn : n < size) : (ofNat n).toUInt32 = UInt32.ofNat n

@[simp]

theorem UInt16.toUInt64_ofNat' {n : Nat} (hn : n < size) : (ofNat n).toUInt64 = UInt64.ofNat n

@[simp]

theorem UInt16.toUSize_ofNat' {n : Nat} (hn : n < size) : (ofNat n).toUSize = USize.ofNat n

@[simp]

theorem UInt32.toUInt64_ofNat' {n : Nat} (hn : n < size) : (ofNat n).toUInt64 = UInt64.ofNat n

@[simp]

theorem UInt32.toUSize_ofNat' {n : Nat} (hn : n < size) : (ofNat n).toUSize = USize.ofNat n

@[simp]

theorem USize.toUInt64_ofNat' {n : Nat} (hn : n < size) : (ofNat n).toUInt64 = UInt64.ofNat n

@[simp]

theorem UInt8.toUInt16_ofNat {n : Nat} (hn : n < 256) : (OfNat.ofNat n).toUInt16 = OfNat.ofNat n

@[simp]

theorem UInt8.toUInt32_ofNat {n : Nat} (hn : n < 256) : (OfNat.ofNat n).toUInt32 = OfNat.ofNat n

@[simp]

theorem UInt8.toUInt64_ofNat {n : Nat} (hn : n < 256) : (OfNat.ofNat n).toUInt64 = OfNat.ofNat n

@[simp]

theorem UInt8.toUSize_ofNat {n : Nat} (hn : n < 256) : (OfNat.ofNat n).toUSize = OfNat.ofNat n

@[simp]

theorem UInt16.toUInt32_ofNat {n : Nat} (hn : n < 65536) : (OfNat.ofNat n).toUInt32 = OfNat.ofNat n

@[simp]

theorem UInt16.toUInt64_ofNat {n : Nat} (hn : n < 65536) : (OfNat.ofNat n).toUInt64 = OfNat.ofNat n

@[simp]

theorem UInt16.toUSize_ofNat {n : Nat} (hn : n < 65536) : (OfNat.ofNat n).toUSize = OfNat.ofNat n

@[simp]

theorem UInt32.toUInt64_ofNat {n : Nat} (hn : n < 4294967296) : (OfNat.ofNat n).toUInt64 = OfNat.ofNat n

@[simp]

theorem UInt32.toUSize_ofNat {n : Nat} (hn : n < 4294967296) : (OfNat.ofNat n).toUSize = OfNat.ofNat n

@[simp]

theorem USize.toUInt64_ofNat {n : Nat} (hn : n < 4294967296) : (OfNat.ofNat n).toUInt64 = OfNat.ofNat n

@[simp]

theorem UInt8.ofNatLT_finVal (n : Fin size) : ofNatLT ↑n ⋯ = ofFin n

@[simp]

theorem UInt16.ofNatLT_finVal (n : Fin size) : ofNatLT ↑n ⋯ = ofFin n

@[simp]

theorem UInt32.ofNatLT_finVal (n : Fin size) : ofNatLT ↑n ⋯ = ofFin n

@[simp]

theorem UInt64.ofNatLT_finVal (n : Fin size) : ofNatLT ↑n ⋯ = ofFin n

@[simp]

theorem USize.ofNatLT_finVal (n : Fin size) : ofNatLT ↑n ⋯ = ofFin n

@[simp]

theorem UInt8.ofNatLT_bitVecToNat (n : BitVec 8) : ofNatLT n.toNat ⋯ = { toBitVec := n }

@[simp]

theorem UInt16.ofNatLT_bitVecToNat (n : BitVec 16) : ofNatLT n.toNat ⋯ = { toBitVec := n }

@[simp]

theorem UInt32.ofNatLT_bitVecToNat (n : BitVec 32) : ofNatLT n.toNat ⋯ = { toBitVec := n }

@[simp]

theorem UInt64.ofNatLT_bitVecToNat (n : BitVec 64) : ofNatLT n.toNat ⋯ = { toBitVec := n }

@[simp]

theorem USize.ofNatLT_bitVecToNat (n : BitVec System.Platform.numBits) : ofNatLT n.toNat ⋯ = { toBitVec := n }

@[simp]

theorem UInt8.ofNat_finVal (n : Fin size) : ofNat ↑n = ofFin n

@[simp]

theorem UInt16.ofNat_finVal (n : Fin size) : ofNat ↑n = ofFin n

@[simp]

theorem UInt32.ofNat_finVal (n : Fin size) : ofNat ↑n = ofFin n

@[simp]

theorem UInt64.ofNat_finVal (n : Fin size) : ofNat ↑n = ofFin n

@[simp]

theorem USize.ofNat_finVal (n : Fin size) : ofNat ↑n = ofFin n

@[simp]

theorem UInt8.ofNat_bitVecToNat (n : BitVec 8) : ofNat n.toNat = { toBitVec := n }

@[simp]

theorem UInt16.ofNat_bitVecToNat (n : BitVec 16) : ofNat n.toNat = { toBitVec := n }

@[simp]

theorem UInt32.ofNat_bitVecToNat (n : BitVec 32) : ofNat n.toNat = { toBitVec := n }

@[simp]

theorem UInt64.ofNat_bitVecToNat (n : BitVec 64) : ofNat n.toNat = { toBitVec := n }

@[simp]

theorem USize.ofNat_bitVecToNat (n : BitVec System.Platform.numBits) : ofNat n.toNat = { toBitVec := n }

@[simp]

theorem UInt8.ofNatClamp_finVal (n : Fin size) : ofNatClamp ↑n = ofFin n

@[simp]

theorem UInt16.ofNatClamp_finVal (n : Fin size) : ofNatClamp ↑n = ofFin n

@[simp]

theorem UInt32.ofNatClamp_finVal (n : Fin size) : ofNatClamp ↑n = ofFin n

@[simp]

theorem UInt64.ofNatClamp_finVal (n : Fin size) : ofNatClamp ↑n = ofFin n

@[simp]

theorem USize.ofNatClamp_finVal (n : Fin size) : ofNatClamp ↑n = ofFin n

@[simp]

theorem UInt8.ofNatClamp_bitVecToNat (n : BitVec 8) : ofNatClamp n.toNat = { toBitVec := n }

@[simp]

theorem UInt16.ofNatClamp_bitVecToNat (n : BitVec 16) : ofNatClamp n.toNat = { toBitVec := n }

@[simp]

theorem UInt32.ofNatClamp_bitVecToNat (n : BitVec 32) : ofNatClamp n.toNat = { toBitVec := n }

@[simp]

theorem UInt64.ofNatClamp_bitVecToNat (n : BitVec 64) : ofNatClamp n.toNat = { toBitVec := n }

@[simp]

theorem USize.ofNatClamp_bitVecToNat (n : BitVec System.Platform.numBits) : ofNatClamp n.toNat = { toBitVec := n }

@[deprecated UInt8.ofNatClamp_eq_ofNat (since := "2026-05-04")]

theorem UInt8.ofNatTruncate_eq_ofNat (n : Nat) (hn : n < size) : ofNatClamp n = ofNat n

@[deprecated UInt16.ofNatClamp_eq_ofNat (since := "2026-05-04")]

theorem UInt16.ofNatTruncate_eq_ofNat (n : Nat) (hn : n < size) : ofNatClamp n = ofNat n

@[deprecated UInt32.ofNatClamp_eq_ofNat (since := "2026-05-04")]

theorem UInt32.ofNatTruncate_eq_ofNat (n : Nat) (hn : n < size) : ofNatClamp n = ofNat n

@[deprecated UInt64.ofNatClamp_eq_ofNat (since := "2026-05-04")]

theorem UInt64.ofNatTruncate_eq_ofNat (n : Nat) (hn : n < size) : ofNatClamp n = ofNat n

@[deprecated USize.ofNatClamp_eq_ofNat (since := "2026-05-04")]

theorem USize.ofNatTruncate_eq_ofNat (n : Nat) (hn : n < size) : ofNatClamp n = ofNat n

@[deprecated UInt8.ofNatClamp_toNat (since := "2026-05-04")]

theorem UInt8.ofNatTruncate_toNat (n : UInt8) : ofNatClamp n.toNat = n

@[deprecated UInt16.ofNatClamp_uInt8ToNat (since := "2026-05-04")]

theorem UInt16.ofNatTruncate_uInt8ToNat (n : UInt8) : ofNatClamp n.toNat = n.toUInt16

@[deprecated UInt16.ofNatClamp_toNat (since := "2026-05-04")]

theorem UInt16.ofNatTruncate_toNat (n : UInt16) : ofNatClamp n.toNat = n

@[deprecated UInt32.ofNatClamp_uInt8ToNat (since := "2026-05-04")]

theorem UInt32.ofNatTruncate_uInt8ToNat (n : UInt8) : ofNatClamp n.toNat = n.toUInt32

@[deprecated UInt32.ofNatClamp_uInt16ToNat (since := "2026-05-04")]

theorem UInt32.ofNatTruncate_uInt16ToNat (n : UInt16) : ofNatClamp n.toNat = n.toUInt32

@[deprecated UInt32.ofNatClamp_toNat (since := "2026-05-04")]

theorem UInt32.ofNatTruncate_toNat (n : UInt32) : ofNatClamp n.toNat = n

@[deprecated UInt64.ofNatClamp_uInt8ToNat (since := "2026-05-04")]

theorem UInt64.ofNatTruncate_uInt8ToNat (n : UInt8) : ofNatClamp n.toNat = n.toUInt64

@[deprecated UInt64.ofNatClamp_uInt16ToNat (since := "2026-05-04")]

theorem UInt64.ofNatTruncate_uInt16ToNat (n : UInt16) : ofNatClamp n.toNat = n.toUInt64

@[deprecated UInt64.ofNatClamp_uInt32ToNat (since := "2026-05-04")]

theorem UInt64.ofNatTruncate_uInt32ToNat (n : UInt32) : ofNatClamp n.toNat = n.toUInt64

@[deprecated UInt64.ofNatClamp_toNat (since := "2026-05-04")]

theorem UInt64.ofNatTruncate_toNat (n : UInt64) : ofNatClamp n.toNat = n

@[deprecated UInt64.ofNatClamp_uSizeToNat (since := "2026-05-04")]

theorem UInt64.ofNatTruncate_uSizeToNat (n : USize) : ofNatClamp n.toNat = n.toUInt64

@[deprecated USize.ofNatClamp_uInt8ToNat (since := "2026-05-04")]

theorem USize.ofNatTruncate_uInt8ToNat (n : UInt8) : ofNatClamp n.toNat = n.toUSize

@[deprecated USize.ofNatClamp_uInt16ToNat (since := "2026-05-04")]

theorem USize.ofNatTruncate_uInt16ToNat (n : UInt16) : ofNatClamp n.toNat = n.toUSize

@[deprecated USize.ofNatClamp_uInt32ToNat (since := "2026-05-04")]

theorem USize.ofNatTruncate_uInt32ToNat (n : UInt32) : ofNatClamp n.toNat = n.toUSize

@[deprecated USize.ofNatClamp_toNat (since := "2026-05-04")]

theorem USize.ofNatTruncate_toNat (n : USize) : ofNatClamp n.toNat = n

@[deprecated UInt8.toNat_ofNatClamp_of_lt (since := "2026-05-04")]

theorem UInt8.toNat_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toNat = n

@[deprecated UInt16.toNat_ofNatClamp_of_lt (since := "2026-05-04")]

theorem UInt16.toNat_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toNat = n

@[deprecated UInt32.toNat_ofNatClamp_of_lt (since := "2026-05-04")]

theorem UInt32.toNat_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toNat = n

@[deprecated UInt64.toNat_ofNatClamp_of_lt (since := "2026-05-04")]

theorem UInt64.toNat_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toNat = n

@[deprecated USize.toNat_ofNatClamp_of_lt (since := "2026-05-04")]

theorem USize.toNat_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toNat = n

@[deprecated UInt8.toNat_ofNatClamp_of_le (since := "2026-05-04")]

theorem UInt8.toNat_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toNat = size - 1

@[deprecated UInt16.toNat_ofNatClamp_of_le (since := "2026-05-04")]

theorem UInt16.toNat_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toNat = size - 1

@[deprecated UInt32.toNat_ofNatClamp_of_le (since := "2026-05-04")]

theorem UInt32.toNat_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toNat = size - 1

@[deprecated UInt64.toNat_ofNatClamp_of_le (since := "2026-05-04")]

theorem UInt64.toNat_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toNat = size - 1

@[deprecated USize.toNat_ofNatClamp_of_le (since := "2026-05-04")]

theorem USize.toNat_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toNat = size - 1

@[deprecated UInt8.toFin_ofNatClamp_of_lt (since := "2026-05-04")]

theorem UInt8.toFin_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toFin = ⟨n, hn⟩

@[deprecated UInt16.toFin_ofNatClamp_of_lt (since := "2026-05-04")]

theorem UInt16.toFin_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toFin = ⟨n, hn⟩

@[deprecated UInt32.toFin_ofNatClamp_of_lt (since := "2026-05-04")]

theorem UInt32.toFin_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toFin = ⟨n, hn⟩

@[deprecated UInt64.toFin_ofNatClamp_of_lt (since := "2026-05-04")]

theorem UInt64.toFin_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toFin = ⟨n, hn⟩

@[deprecated USize.toFin_ofNatClamp_of_lt (since := "2026-05-04")]

theorem USize.toFin_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toFin = ⟨n, hn⟩

@[deprecated UInt8.toFin_ofNatClamp_of_le (since := "2026-05-04")]

theorem UInt8.toFin_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toFin = ⟨size - 1, toFin_ofNatClamp_of_le._proof_1⟩

@[deprecated UInt16.toFin_ofNatClamp_of_le (since := "2026-05-04")]

theorem UInt16.toFin_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toFin = ⟨size - 1, toFin_ofNatClamp_of_le._proof_1⟩

@[deprecated UInt32.toFin_ofNatClamp_of_le (since := "2026-05-04")]

theorem UInt32.toFin_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toFin = ⟨size - 1, toFin_ofNatClamp_of_le._proof_1⟩

@[deprecated UInt64.toFin_ofNatClamp_of_le (since := "2026-05-04")]

theorem UInt64.toFin_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toFin = ⟨size - 1, toFin_ofNatClamp_of_le._proof_1⟩

@[deprecated USize.toFin_ofNatClamp_of_le (since := "2026-05-04")]

theorem USize.toFin_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toFin = ⟨size - 1, toFin_ofNatClamp_of_le._proof_1⟩

@[deprecated UInt8.toBitVec_ofNatClamp_of_lt (since := "2026-05-04")]

theorem UInt8.toBitVec_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toBitVec = n#'hn

@[deprecated UInt16.toBitVec_ofNatClamp_of_lt (since := "2026-05-04")]

theorem UInt16.toBitVec_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toBitVec = n#'hn

@[deprecated UInt32.toBitVec_ofNatClamp_of_lt (since := "2026-05-04")]

theorem UInt32.toBitVec_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toBitVec = n#'hn

@[deprecated UInt64.toBitVec_ofNatClamp_of_lt (since := "2026-05-04")]

theorem UInt64.toBitVec_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toBitVec = n#'hn

@[deprecated USize.toBitVec_ofNatClamp_of_lt (since := "2026-05-04")]

theorem USize.toBitVec_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toBitVec = n#'hn

@[deprecated UInt8.toBitVec_ofNatClamp_of_le (since := "2026-05-04")]

theorem UInt8.toBitVec_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toBitVec = (size - 1)#'toBitVec_ofNatClamp_of_le._proof_1

@[deprecated UInt16.toBitVec_ofNatClamp_of_le (since := "2026-05-04")]

theorem UInt16.toBitVec_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toBitVec = (size - 1)#'toBitVec_ofNatClamp_of_le._proof_1

@[deprecated UInt32.toBitVec_ofNatClamp_of_le (since := "2026-05-04")]

theorem UInt32.toBitVec_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toBitVec = (size - 1)#'toBitVec_ofNatClamp_of_le._proof_1

@[deprecated UInt64.toBitVec_ofNatClamp_of_le (since := "2026-05-04")]

theorem UInt64.toBitVec_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toBitVec = (size - 1)#'toBitVec_ofNatClamp_of_le._proof_1

@[deprecated USize.toBitVec_ofNatClamp_of_le (since := "2026-05-04")]

theorem USize.toBitVec_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toBitVec = (size - 1)#'toBitVec_ofNatClamp_of_le._proof_1

@[deprecated UInt16.toUInt8_ofNatClamp_of_lt (since := "2026-05-04")]

theorem UInt16.toUInt8_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt8 = UInt8.ofNat n

@[deprecated UInt32.toUInt8_ofNatClamp_of_lt (since := "2026-05-04")]

theorem UInt32.toUInt8_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt8 = UInt8.ofNat n

@[deprecated UInt64.toUInt8_ofNatClamp_of_lt (since := "2026-05-04")]

theorem UInt64.toUInt8_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt8 = UInt8.ofNat n

@[deprecated USize.toUInt8_ofNatClamp_of_lt (since := "2026-05-04")]

theorem USize.toUInt8_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt8 = UInt8.ofNat n

@[deprecated UInt16.toUInt8_ofNatClamp_of_le (since := "2026-05-04")]

theorem UInt16.toUInt8_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt8 = UInt8.ofNatLT (UInt8.size - 1) toUInt8_ofNatClamp_of_le._proof_1

@[deprecated UInt32.toUInt8_ofNatClamp_of_le (since := "2026-05-04")]

theorem UInt32.toUInt8_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt8 = UInt8.ofNatLT (UInt8.size - 1) UInt16.toUInt8_ofNatClamp_of_le._proof_1

@[deprecated UInt64.toUInt8_ofNatClamp_of_le (since := "2026-05-04")]

theorem UInt64.toUInt8_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt8 = UInt8.ofNatLT (UInt8.size - 1) UInt16.toUInt8_ofNatClamp_of_le._proof_1

@[deprecated USize.toUInt8_ofNatClamp_of_le (since := "2026-05-04")]

theorem USize.toUInt8_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt8 = UInt8.ofNatLT (UInt8.size - 1) UInt16.toUInt8_ofNatClamp_of_le._proof_1

@[deprecated UInt32.toUInt16_ofNatClamp_of_lt (since := "2026-05-04")]

theorem UInt32.toUInt16_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt16 = UInt16.ofNat n

@[deprecated UInt64.toUInt16_ofNatClamp_of_lt (since := "2026-05-04")]

theorem UInt64.toUInt16_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt16 = UInt16.ofNat n

@[deprecated USize.toUInt16_ofNatClamp_of_lt (since := "2026-05-04")]

theorem USize.toUInt16_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt16 = UInt16.ofNat n

@[deprecated UInt32.toUInt16_ofNatClamp_of_le (since := "2026-05-04")]

theorem UInt32.toUInt16_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt16 = UInt16.ofNatLT (UInt16.size - 1) toUInt16_ofNatClamp_of_le._proof_1

@[deprecated UInt64.toUInt16_ofNatClamp_of_le (since := "2026-05-04")]

theorem UInt64.toUInt16_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt16 = UInt16.ofNatLT (UInt16.size - 1) UInt32.toUInt16_ofNatClamp_of_le._proof_1

@[deprecated USize.toUInt16_ofNatClamp_of_le (since := "2026-05-04")]

theorem USize.toUInt16_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt16 = UInt16.ofNatLT (UInt16.size - 1) UInt32.toUInt16_ofNatClamp_of_le._proof_1

@[deprecated UInt64.toUInt32_ofNatClamp_of_lt (since := "2026-05-04")]

theorem UInt64.toUInt32_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt32 = UInt32.ofNat n

@[deprecated USize.toUInt32_ofNatClamp_of_lt (since := "2026-05-04")]

theorem USize.toUInt32_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt32 = UInt32.ofNat n

@[deprecated UInt64.toUInt32_ofNatClamp_of_le (since := "2026-05-04")]

theorem UInt64.toUInt32_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt32 = UInt32.ofNatLT (UInt32.size - 1) toUInt32_ofNatClamp_of_le._proof_1

@[deprecated USize.toUInt32_ofNatClamp_of_le (since := "2026-05-04")]

theorem USize.toUInt32_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt32 = UInt32.ofNatLT (UInt32.size - 1) UInt64.toUInt32_ofNatClamp_of_le._proof_1

@[deprecated UInt64.toUSize_ofNatClamp_of_lt (since := "2026-05-04")]

theorem UInt64.toUSize_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUSize = USize.ofNat n

@[deprecated UInt64.toUSize_ofNatClamp_of_le (since := "2026-05-04")]

theorem UInt64.toUSize_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUSize = USize.ofNatLT (USize.size - 1) toUSize_ofNatClamp_of_le._proof_1

@[deprecated UInt8.toUInt16_ofNatClamp_of_lt (since := "2026-05-04")]

theorem UInt8.toUInt16_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt16 = UInt16.ofNatLT n ⋯

@[deprecated UInt8.toUInt32_ofNatClamp_of_lt (since := "2026-05-04")]

theorem UInt8.toUInt32_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt32 = UInt32.ofNatLT n ⋯

@[deprecated UInt8.toUInt64_ofNatClamp_of_lt (since := "2026-05-04")]

theorem UInt8.toUInt64_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt64 = UInt64.ofNatLT n ⋯

@[deprecated UInt8.toUSize_ofNatClamp_of_lt (since := "2026-05-04")]

theorem UInt8.toUSize_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUSize = USize.ofNatLT n ⋯

@[deprecated UInt8.toUInt16_ofNatClamp_of_le (since := "2026-05-04")]

theorem UInt8.toUInt16_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt16 = UInt16.ofNatLT (size - 1) toUInt16_ofNatClamp_of_le._proof_1

@[deprecated UInt8.toUInt32_ofNatClamp_of_le (since := "2026-05-04")]

theorem UInt8.toUInt32_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt32 = UInt32.ofNatLT (size - 1) toUInt32_ofNatClamp_of_le._proof_1

@[deprecated UInt8.toUInt64_ofNatClamp_of_le (since := "2026-05-04")]

theorem UInt8.toUInt64_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt64 = UInt64.ofNatLT (size - 1) toUInt64_ofNatClamp_of_le._proof_1

@[deprecated UInt8.toUSize_ofNatClamp_of_le (since := "2026-05-04")]

theorem UInt8.toUSize_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUSize = USize.ofNatLT (size - 1) ⋯

@[deprecated UInt16.toUInt32_ofNatClamp_of_lt (since := "2026-05-04")]

theorem UInt16.toUInt32_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt32 = UInt32.ofNatLT n ⋯

@[deprecated UInt16.toUInt64_ofNatClamp_of_lt (since := "2026-05-04")]

theorem UInt16.toUInt64_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt64 = UInt64.ofNatLT n ⋯

@[deprecated UInt16.toUSize_ofNatClamp_of_lt (since := "2026-05-04")]

theorem UInt16.toUSize_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUSize = USize.ofNatLT n ⋯

@[deprecated UInt16.toUInt32_ofNatClamp_of_le (since := "2026-05-04")]

theorem UInt16.toUInt32_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt32 = UInt32.ofNatLT (size - 1) toUInt32_ofNatClamp_of_le._proof_1

@[deprecated UInt16.toUInt64_ofNatClamp_of_le (since := "2026-05-04")]

theorem UInt16.toUInt64_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt64 = UInt64.ofNatLT (size - 1) toUInt64_ofNatClamp_of_le._proof_1

@[deprecated UInt16.toUSize_ofNatClamp_of_le (since := "2026-05-04")]

theorem UInt16.toUSize_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUSize = USize.ofNatLT (size - 1) ⋯

@[deprecated UInt32.toUInt64_ofNatClamp_of_lt (since := "2026-05-04")]

theorem UInt32.toUInt64_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt64 = UInt64.ofNatLT n ⋯

@[deprecated UInt32.toUSize_ofNatClamp_of_lt (since := "2026-05-04")]

theorem UInt32.toUSize_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUSize = USize.ofNatLT n ⋯

@[deprecated UInt32.toUInt64_ofNatClamp_of_le (since := "2026-05-04")]

theorem UInt32.toUInt64_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt64 = UInt64.ofNatLT (size - 1) toUInt64_ofNatClamp_of_le._proof_1

@[deprecated UInt32.toUSize_ofNatClamp_of_le (since := "2026-05-04")]

theorem UInt32.toUSize_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUSize = USize.ofNatLT (size - 1) ⋯

@[deprecated USize.toUInt64_ofNatClamp_of_lt (since := "2026-05-04")]

theorem USize.toUInt64_ofNatTruncate_of_lt {n : Nat} (hn : n < size) : (ofNatClamp n).toUInt64 = UInt64.ofNatLT n ⋯

@[deprecated USize.toUInt64_ofNatClamp_of_le (since := "2026-05-04")]

theorem USize.toUInt64_ofNatTruncate_of_le {n : Nat} (hn : size ≤ n) : (ofNatClamp n).toUInt64 = UInt64.ofNatLT (size - 1) toUInt64_ofNatClamp_of_le._proof_1

@[deprecated UInt8.ofNatClamp_finVal (since := "2026-05-04")]

theorem UInt8.ofNatTruncate_finVal (n : Fin size) : ofNatClamp ↑n = ofFin n

@[deprecated UInt16.ofNatClamp_finVal (since := "2026-05-04")]

theorem UInt16.ofNatTruncate_finVal (n : Fin size) : ofNatClamp ↑n = ofFin n

@[deprecated UInt32.ofNatClamp_finVal (since := "2026-05-04")]

theorem UInt32.ofNatTruncate_finVal (n : Fin size) : ofNatClamp ↑n = ofFin n

@[deprecated UInt64.ofNatClamp_finVal (since := "2026-05-04")]

theorem UInt64.ofNatTruncate_finVal (n : Fin size) : ofNatClamp ↑n = ofFin n

@[deprecated USize.ofNatClamp_finVal (since := "2026-05-04")]

theorem USize.ofNatTruncate_finVal (n : Fin size) : ofNatClamp ↑n = ofFin n

@[deprecated UInt8.ofNatClamp_bitVecToNat (since := "2026-05-04")]

theorem UInt8.ofNatTruncate_bitVecToNat (n : BitVec 8) : ofNatClamp n.toNat = { toBitVec := n }

@[deprecated UInt16.ofNatClamp_bitVecToNat (since := "2026-05-04")]

theorem UInt16.ofNatTruncate_bitVecToNat (n : BitVec 16) : ofNatClamp n.toNat = { toBitVec := n }

@[deprecated UInt32.ofNatClamp_bitVecToNat (since := "2026-05-04")]

theorem UInt32.ofNatTruncate_bitVecToNat (n : BitVec 32) : ofNatClamp n.toNat = { toBitVec := n }

@[deprecated UInt64.ofNatClamp_bitVecToNat (since := "2026-05-04")]

theorem UInt64.ofNatTruncate_bitVecToNat (n : BitVec 64) : ofNatClamp n.toNat = { toBitVec := n }

@[deprecated USize.ofNatClamp_bitVecToNat (since := "2026-05-04")]

theorem USize.ofNatTruncate_bitVecToNat (n : BitVec System.Platform.numBits) : ofNatClamp n.toNat = { toBitVec := n }

@[simp]

theorem UInt8.ofFin_mk {n : Nat} (hn : n < size) : ofFin ⟨n, hn⟩ = ofNatLT n hn

@[simp]

theorem UInt16.ofFin_mk {n : Nat} (hn : n < size) : ofFin ⟨n, hn⟩ = ofNatLT n hn

@[simp]

theorem UInt32.ofFin_mk {n : Nat} (hn : n < size) : ofFin ⟨n, hn⟩ = ofNatLT n hn

@[simp]

theorem UInt64.ofFin_mk {n : Nat} (hn : n < size) : ofFin ⟨n, hn⟩ = ofNatLT n hn

@[simp]

theorem USize.ofFin_mk {n : Nat} (hn : n < size) : ofFin ⟨n, hn⟩ = ofNatLT n hn

@[simp]

theorem UInt8.ofFin_bitVecToFin (n : BitVec 8) : ofFin n.toFin = { toBitVec := n }

@[simp]

theorem UInt16.ofFin_bitVecToFin (n : BitVec 16) : ofFin n.toFin = { toBitVec := n }

@[simp]

theorem UInt32.ofFin_bitVecToFin (n : BitVec 32) : ofFin n.toFin = { toBitVec := n }

@[simp]

theorem UInt64.ofFin_bitVecToFin (n : BitVec 64) : ofFin n.toFin = { toBitVec := n }

@[simp]

theorem USize.ofFin_bitVecToFin (n : BitVec System.Platform.numBits) : ofFin n.toFin = { toBitVec := n }

@[simp]

theorem UInt8.ofBitVec_ofNatLT {n : Nat} (hn : n < 2 ^ 8) : { toBitVec := n#'hn } = ofNatLT n hn

@[simp]

theorem UInt16.ofBitVec_ofNatLT {n : Nat} (hn : n < 2 ^ 16) : { toBitVec := n#'hn } = ofNatLT n hn

@[simp]

theorem UInt32.ofBitVec_ofNatLT {n : Nat} (hn : n < 2 ^ 32) : { toBitVec := n#'hn } = ofNatLT n hn

@[simp]

theorem UInt64.ofBitVec_ofNatLT {n : Nat} (hn : n < 2 ^ 64) : { toBitVec := n#'hn } = ofNatLT n hn

@[simp]

theorem USize.ofBitVec_ofNatLT {n : Nat} (hn : n < 2 ^ System.Platform.numBits) : { toBitVec := n#'hn } = ofNatLT n hn

@[simp]

theorem UInt8.ofBitVec_ofFin (n : Fin (2 ^ 8)) : { toBitVec := { toFin := n } } = ofFin n

@[simp]

theorem UInt16.ofBitVec_ofFin (n : Fin (2 ^ 16)) : { toBitVec := { toFin := n } } = ofFin n

@[simp]

theorem UInt32.ofBitVec_ofFin (n : Fin (2 ^ 32)) : { toBitVec := { toFin := n } } = ofFin n

@[simp]

theorem UInt64.ofBitVec_ofFin (n : Fin (2 ^ 64)) : { toBitVec := { toFin := n } } = ofFin n

@[simp]

theorem USize.ofBitVec_ofFin (n : Fin (2 ^ System.Platform.numBits)) : { toBitVec := { toFin := n } } = ofFin n

@[simp]

theorem BitVec.ofNat_uInt8ToNat (n : UInt8) : BitVec.ofNat 8 n.toNat = n.toBitVec

@[simp]

theorem BitVec.ofNat_uInt16ToNat (n : UInt16) : BitVec.ofNat 16 n.toNat = n.toBitVec

@[simp]

theorem BitVec.ofNat_uInt32ToNat (n : UInt32) : BitVec.ofNat 32 n.toNat = n.toBitVec

@[simp]

theorem BitVec.ofNat_uInt64ToNat (n : UInt64) : BitVec.ofNat 64 n.toNat = n.toBitVec

@[simp]

theorem BitVec.ofNat_uSizeToNat (n : USize) : BitVec.ofNat System.Platform.numBits n.toNat = n.toBitVec

@[simp]

theorem UInt8.toFin_div (a b : UInt8) : (a / b).toFin = a.toFin / b.toFin

@[simp]

theorem UInt16.toFin_div (a b : UInt16) : (a / b).toFin = a.toFin / b.toFin

@[simp]

theorem UInt32.toFin_div (a b : UInt32) : (a / b).toFin = a.toFin / b.toFin

@[simp]

theorem UInt64.toFin_div (a b : UInt64) : (a / b).toFin = a.toFin / b.toFin

@[simp]

theorem USize.toFin_div (a b : USize) : (a / b).toFin = a.toFin / b.toFin

@[simp]

theorem UInt8.toUInt16_div (a b : UInt8) : (a / b).toUInt16 = a.toUInt16 / b.toUInt16

@[simp]

theorem UInt8.toUInt32_div (a b : UInt8) : (a / b).toUInt32 = a.toUInt32 / b.toUInt32

@[simp]

theorem UInt8.toUInt64_div (a b : UInt8) : (a / b).toUInt64 = a.toUInt64 / b.toUInt64

@[simp]

theorem UInt8.toUSize_div (a b : UInt8) : (a / b).toUSize = a.toUSize / b.toUSize

@[simp]

theorem UInt16.toUInt32_div (a b : UInt16) : (a / b).toUInt32 = a.toUInt32 / b.toUInt32

@[simp]

theorem UInt16.toUInt64_div (a b : UInt16) : (a / b).toUInt64 = a.toUInt64 / b.toUInt64

@[simp]

theorem UInt16.toUSize_div (a b : UInt16) : (a / b).toUSize = a.toUSize / b.toUSize

@[simp]

theorem UInt32.toUInt64_div (a b : UInt32) : (a / b).toUInt64 = a.toUInt64 / b.toUInt64

@[simp]

theorem UInt32.toUSize_div (a b : UInt32) : (a / b).toUSize = a.toUSize / b.toUSize

@[simp]

theorem USize.toUInt64_div (a b : USize) : (a / b).toUInt64 = a.toUInt64 / b.toUInt64

theorem UInt16.toUInt8_div (a b : UInt16) (ha : a < 256) (hb : b < 256) : (a / b).toUInt8 = a.toUInt8 / b.toUInt8

theorem UInt32.toUInt8_div (a b : UInt32) (ha : a < 256) (hb : b < 256) : (a / b).toUInt8 = a.toUInt8 / b.toUInt8

theorem UInt32.toUInt16_div (a b : UInt32) (ha : a < 65536) (hb : b < 65536) : (a / b).toUInt16 = a.toUInt16 / b.toUInt16

theorem USize.toUInt8_div (a b : USize) (ha : a < 256) (hb : b < 256) : (a / b).toUInt8 = a.toUInt8 / b.toUInt8

theorem USize.toUInt16_div (a b : USize) (ha : a < 65536) (hb : b < 65536) : (a / b).toUInt16 = a.toUInt16 / b.toUInt16

theorem UInt64.toUInt8_div (a b : UInt64) (ha : a < 256) (hb : b < 256) : (a / b).toUInt8 = a.toUInt8 / b.toUInt8

theorem UInt64.toUInt16_div (a b : UInt64) (ha : a < 65536) (hb : b < 65536) : (a / b).toUInt16 = a.toUInt16 / b.toUInt16

theorem UInt64.toUInt32_div (a b : UInt64) (ha : a < 4294967296) (hb : b < 4294967296) : (a / b).toUInt32 = a.toUInt32 / b.toUInt32

theorem UInt64.toUSize_div (a b : UInt64) (ha : a < 4294967296) (hb : b < 4294967296) : (a / b).toUSize = a.toUSize / b.toUSize

theorem UInt64.toUSize_div_of_toNat_lt (a b : UInt64) (ha : a.toNat < USize.size) (hb : b.toNat < USize.size) : (a / b).toUSize = a.toUSize / b.toUSize

@[simp]

theorem UInt8.toFin_mod (a b : UInt8) : (a % b).toFin = a.toFin % b.toFin

@[simp]

theorem UInt16.toFin_mod (a b : UInt16) : (a % b).toFin = a.toFin % b.toFin

@[simp]

theorem UInt32.toFin_mod (a b : UInt32) : (a % b).toFin = a.toFin % b.toFin

@[simp]

theorem UInt64.toFin_mod (a b : UInt64) : (a % b).toFin = a.toFin % b.toFin

@[simp]

theorem USize.toFin_mod (a b : USize) : (a % b).toFin = a.toFin % b.toFin

@[simp]

theorem UInt8.toUInt16_mod (a b : UInt8) : (a % b).toUInt16 = a.toUInt16 % b.toUInt16

@[simp]

theorem UInt8.toUInt32_mod (a b : UInt8) : (a % b).toUInt32 = a.toUInt32 % b.toUInt32

@[simp]

theorem UInt8.toUInt64_mod (a b : UInt8) : (a % b).toUInt64 = a.toUInt64 % b.toUInt64

@[simp]

theorem UInt8.toUSize_mod (a b : UInt8) : (a % b).toUSize = a.toUSize % b.toUSize

@[simp]

theorem UInt16.toUInt32_mod (a b : UInt16) : (a % b).toUInt32 = a.toUInt32 % b.toUInt32

@[simp]

theorem UInt16.toUInt64_mod (a b : UInt16) : (a % b).toUInt64 = a.toUInt64 % b.toUInt64

@[simp]

theorem UInt16.toUSize_mod (a b : UInt16) : (a % b).toUSize = a.toUSize % b.toUSize

@[simp]

theorem UInt32.toUInt64_mod (a b : UInt32) : (a % b).toUInt64 = a.toUInt64 % b.toUInt64

@[simp]

theorem UInt32.toUSize_mod (a b : UInt32) : (a % b).toUSize = a.toUSize % b.toUSize

@[simp]

theorem USize.toUInt64_mod (a b : USize) : (a % b).toUInt64 = a.toUInt64 % b.toUInt64

theorem UInt16.toUInt8_mod (a b : UInt16) (ha : a < 256) (hb : b < 256) : (a % b).toUInt8 = a.toUInt8 % b.toUInt8

theorem UInt16.toUInt8_mod_of_dvd (a b : UInt16) (hb : b.toNat ∣ 256) : (a % b).toUInt8 = a.toUInt8 % b.toUInt8

theorem UInt32.toUInt8_mod (a b : UInt32) (ha : a < 256) (hb : b < 256) : (a % b).toUInt8 = a.toUInt8 % b.toUInt8

theorem UInt32.toUInt16_mod (a b : UInt32) (ha : a < 65536) (hb : b < 65536) : (a % b).toUInt16 = a.toUInt16 % b.toUInt16

theorem UInt32.toUInt8_mod_of_dvd (a b : UInt32) (hb : b.toNat ∣ 256) : (a % b).toUInt8 = a.toUInt8 % b.toUInt8

theorem UInt32.toUInt16_mod_of_dvd (a b : UInt32) (hb : b.toNat ∣ 65536) : (a % b).toUInt16 = a.toUInt16 % b.toUInt16

theorem USize.toUInt8_mod (a b : USize) (ha : a < 256) (hb : b < 256) : (a % b).toUInt8 = a.toUInt8 % b.toUInt8

theorem USize.toUInt16_mod (a b : USize) (ha : a < 65536) (hb : b < 65536) : (a % b).toUInt16 = a.toUInt16 % b.toUInt16

theorem USize.toUInt32_mod (a b : USize) (ha : a < 4294967296) (hb : b < 4294967296) : (a % b).toUInt32 = a.toUInt32 % b.toUInt32

theorem USize.toUInt8_mod_of_dvd (a b : USize) (hb : b.toNat ∣ 256) : (a % b).toUInt8 = a.toUInt8 % b.toUInt8

theorem USize.toUInt16_mod_of_dvd (a b : USize) (hb : b.toNat ∣ 65536) : (a % b).toUInt16 = a.toUInt16 % b.toUInt16

theorem USize.toUInt32_mod_of_dvd (a b : USize) (hb : b.toNat ∣ 4294967296) : (a % b).toUInt32 = a.toUInt32 % b.toUInt32

theorem UInt64.toUInt8_mod (a b : UInt64) (ha : a < 256) (hb : b < 256) : (a % b).toUInt8 = a.toUInt8 % b.toUInt8

theorem UInt64.toUInt16_mod (a b : UInt64) (ha : a < 65536) (hb : b < 65536) : (a % b).toUInt16 = a.toUInt16 % b.toUInt16

theorem UInt64.toUInt32_mod (a b : UInt64) (ha : a < 4294967296) (hb : b < 4294967296) : (a % b).toUInt32 = a.toUInt32 % b.toUInt32

theorem UInt64.toUSize_mod (a b : UInt64) (ha : a < 4294967296) (hb : b < 4294967296) : (a % b).toUSize = a.toUSize % b.toUSize

theorem UInt64.toUSize_mod_of_toNat_lt (a b : UInt64) (ha : a.toNat < USize.size) (hb : b.toNat < USize.size) : (a % b).toUSize = a.toUSize % b.toUSize

theorem UInt64.toUInt8_mod_of_dvd (a b : UInt64) (hb : b.toNat ∣ 256) : (a % b).toUInt8 = a.toUInt8 % b.toUInt8

theorem UInt64.toUInt16_mod_of_dvd (a b : UInt64) (hb : b.toNat ∣ 65536) : (a % b).toUInt16 = a.toUInt16 % b.toUInt16

theorem UInt64.toUInt32_mod_of_dvd (a b : UInt64) (hb : b.toNat ∣ 4294967296) : (a % b).toUInt32 = a.toUInt32 % b.toUInt32

theorem UInt64.toUSize_mod_of_dvd (a b : UInt64) (hb : b.toNat ∣ 4294967296) : (a % b).toUSize = a.toUSize % b.toUSize

theorem UInt64.toUSize_mod_of_dvd_usizeSize (a b : UInt64) (hb : b.toNat ∣ USize.size) : (a % b).toUSize = a.toUSize % b.toUSize

@[simp]

theorem UInt8.toFin_add (a b : UInt8) : (a + b).toFin = a.toFin + b.toFin

@[simp]

theorem UInt16.toFin_add (a b : UInt16) : (a + b).toFin = a.toFin + b.toFin

@[simp]

theorem UInt32.toFin_add (a b : UInt32) : (a + b).toFin = a.toFin + b.toFin

@[simp]

theorem UInt64.toFin_add (a b : UInt64) : (a + b).toFin = a.toFin + b.toFin

@[simp]

theorem USize.toFin_add (a b : USize) : (a + b).toFin = a.toFin + b.toFin

@[simp]

theorem UInt16.toUInt8_add (a b : UInt16) : (a + b).toUInt8 = a.toUInt8 + b.toUInt8

@[simp]

theorem UInt32.toUInt8_add (a b : UInt32) : (a + b).toUInt8 = a.toUInt8 + b.toUInt8

@[simp]

theorem UInt64.toUInt8_add (a b : UInt64) : (a + b).toUInt8 = a.toUInt8 + b.toUInt8

@[simp]

theorem USize.toUInt8_add (a b : USize) : (a + b).toUInt8 = a.toUInt8 + b.toUInt8

@[simp]

theorem UInt32.toUInt16_add (a b : UInt32) : (a + b).toUInt16 = a.toUInt16 + b.toUInt16

@[simp]

theorem UInt64.toUInt16_add (a b : UInt64) : (a + b).toUInt16 = a.toUInt16 + b.toUInt16

@[simp]

theorem USize.toUInt16_add (a b : USize) : (a + b).toUInt16 = a.toUInt16 + b.toUInt16

@[simp]

theorem UInt64.toUInt32_add (a b : UInt64) : (a + b).toUInt32 = a.toUInt32 + b.toUInt32

@[simp]

theorem USize.toUInt32_add (a b : USize) : (a + b).toUInt32 = a.toUInt32 + b.toUInt32

@[simp]

theorem UInt64.toUSize_add (a b : UInt64) : (a + b).toUSize = a.toUSize + b.toUSize

@[simp]

theorem UInt8.toUInt16_add (a b : UInt8) : (a + b).toUInt16 = (a.toUInt16 + b.toUInt16) % 256

@[simp]

theorem UInt8.toUInt32_add (a b : UInt8) : (a + b).toUInt32 = (a.toUInt32 + b.toUInt32) % 256

@[simp]

theorem UInt8.toUInt64_add (a b : UInt8) : (a + b).toUInt64 = (a.toUInt64 + b.toUInt64) % 256

@[simp]

theorem UInt8.toUSize_add (a b : UInt8) : (a + b).toUSize = (a.toUSize + b.toUSize) % 256

@[simp]

theorem UInt16.toUInt32_add (a b : UInt16) : (a + b).toUInt32 = (a.toUInt32 + b.toUInt32) % 65536

@[simp]

theorem UInt16.toUInt64_add (a b : UInt16) : (a + b).toUInt64 = (a.toUInt64 + b.toUInt64) % 65536

@[simp]

theorem UInt16.toUSize_add (a b : UInt16) : (a + b).toUSize = (a.toUSize + b.toUSize) % 65536

@[simp]

theorem UInt32.toUInt64_add (a b : UInt32) : (a + b).toUInt64 = (a.toUInt64 + b.toUInt64) % 4294967296

@[simp]

theorem UInt32.toUSize_add (a b : UInt32) : (a + b).toUSize = (a.toUSize + b.toUSize) % 4294967296

Note that on 32-bit machines we are doing a modulo by zero.

@[simp]

theorem UInt8.toFin_sub (a b : UInt8) : (a - b).toFin = a.toFin - b.toFin

@[simp]

theorem UInt16.toFin_sub (a b : UInt16) : (a - b).toFin = a.toFin - b.toFin

@[simp]

theorem UInt32.toFin_sub (a b : UInt32) : (a - b).toFin = a.toFin - b.toFin

@[simp]

theorem UInt64.toFin_sub (a b : UInt64) : (a - b).toFin = a.toFin - b.toFin

@[simp]

theorem USize.toFin_sub (a b : USize) : (a - b).toFin = a.toFin - b.toFin

@[simp]

theorem UInt8.toFin_mul (a b : UInt8) : (a * b).toFin = a.toFin * b.toFin

@[simp]

theorem UInt16.toFin_mul (a b : UInt16) : (a * b).toFin = a.toFin * b.toFin

@[simp]

theorem UInt32.toFin_mul (a b : UInt32) : (a * b).toFin = a.toFin * b.toFin

@[simp]

theorem UInt64.toFin_mul (a b : UInt64) : (a * b).toFin = a.toFin * b.toFin

@[simp]

theorem USize.toFin_mul (a b : USize) : (a * b).toFin = a.toFin * b.toFin

@[simp]

theorem UInt16.toUInt8_mul (a b : UInt16) : (a * b).toUInt8 = a.toUInt8 * b.toUInt8

@[simp]

theorem UInt32.toUInt8_mul (a b : UInt32) : (a * b).toUInt8 = a.toUInt8 * b.toUInt8

@[simp]

theorem UInt64.toUInt8_mul (a b : UInt64) : (a * b).toUInt8 = a.toUInt8 * b.toUInt8

@[simp]

theorem USize.toUInt8_mul (a b : USize) : (a * b).toUInt8 = a.toUInt8 * b.toUInt8

@[simp]

theorem UInt32.toUInt16_mul (a b : UInt32) : (a * b).toUInt16 = a.toUInt16 * b.toUInt16

@[simp]

theorem UInt64.toUInt16_mul (a b : UInt64) : (a * b).toUInt16 = a.toUInt16 * b.toUInt16

@[simp]

theorem USize.toUInt16_mul (a b : USize) : (a * b).toUInt16 = a.toUInt16 * b.toUInt16

@[simp]

theorem UInt64.toUInt32_mul (a b : UInt64) : (a * b).toUInt32 = a.toUInt32 * b.toUInt32

@[simp]

theorem USize.toUInt32_mul (a b : USize) : (a * b).toUInt32 = a.toUInt32 * b.toUInt32

@[simp]

theorem UInt64.toUSize_mul (a b : UInt64) : (a * b).toUSize = a.toUSize * b.toUSize

@[simp]

theorem UInt8.toUInt16_mul (a b : UInt8) : (a * b).toUInt16 = a.toUInt16 * b.toUInt16 % 256

@[simp]

theorem UInt8.toUInt32_mul (a b : UInt8) : (a * b).toUInt32 = a.toUInt32 * b.toUInt32 % 256

@[simp]

theorem UInt8.toUInt64_mul (a b : UInt8) : (a * b).toUInt64 = a.toUInt64 * b.toUInt64 % 256

@[simp]

theorem UInt8.toUSize_mul (a b : UInt8) : (a * b).toUSize = a.toUSize * b.toUSize % 256

@[simp]

theorem UInt16.toUInt32_mul (a b : UInt16) : (a * b).toUInt32 = a.toUInt32 * b.toUInt32 % 65536

@[simp]

theorem UInt16.toUInt64_mul (a b : UInt16) : (a * b).toUInt64 = a.toUInt64 * b.toUInt64 % 65536

@[simp]

theorem UInt16.toUSize_mul (a b : UInt16) : (a * b).toUSize = a.toUSize * b.toUSize % 65536

@[simp]

theorem UInt32.toUInt64_mul (a b : UInt32) : (a * b).toUInt64 = a.toUInt64 * b.toUInt64 % 4294967296

@[simp]

theorem UInt32.toUSize_mul (a b : UInt32) : (a * b).toUSize = a.toUSize * b.toUSize % 4294967296

Note that on 32-bit machines we are doing a modulo by zero.

theorem UInt16.toUInt8_eq (a b : UInt16) : a.toUInt8 = b.toUInt8 ↔ a % 256 = b % 256

theorem UInt32.toUInt8_eq (a b : UInt32) : a.toUInt8 = b.toUInt8 ↔ a % 256 = b % 256

theorem UInt64.toUInt8_eq (a b : UInt64) : a.toUInt8 = b.toUInt8 ↔ a % 256 = b % 256

theorem USize.toUInt8_eq (a b : USize) : a.toUInt8 = b.toUInt8 ↔ a % 256 = b % 256

theorem UInt32.toUInt16_eq (a b : UInt32) : a.toUInt16 = b.toUInt16 ↔ a % 65536 = b % 65536

theorem UInt64.toUInt16_eq (a b : UInt64) : a.toUInt16 = b.toUInt16 ↔ a % 65536 = b % 65536

theorem USize.toUInt16_eq (a b : USize) : a.toUInt16 = b.toUInt16 ↔ a % 65536 = b % 65536

theorem UInt64.toUInt32_eq (a b : UInt64) : a.toUInt32 = b.toUInt32 ↔ a % 4294967296 = b % 4294967296

theorem USize.toUInt32_eq (a b : USize) : a.toUInt32 = b.toUInt32 ↔ a % 4294967296 = b % 4294967296

theorem UInt8.toUInt16_eq_mod_256_iff (a : UInt8) (b : UInt16) : a.toUInt16 = b % 256 ↔ a = b.toUInt8

theorem UInt8.toUInt32_eq_mod_256_iff (a : UInt8) (b : UInt32) : a.toUInt32 = b % 256 ↔ a = b.toUInt8

theorem UInt8.toUInt64_eq_mod_256_iff (a : UInt8) (b : UInt64) : a.toUInt64 = b % 256 ↔ a = b.toUInt8

theorem UInt8.toUSize_eq_mod_256_iff (a : UInt8) (b : USize) : a.toUSize = b % 256 ↔ a = b.toUInt8

theorem UInt16.toUInt32_eq_mod_65536_iff (a : UInt16) (b : UInt32) : a.toUInt32 = b % 65536 ↔ a = b.toUInt16

theorem UInt16.toUInt64_eq_mod_65536_iff (a : UInt16) (b : UInt64) : a.toUInt64 = b % 65536 ↔ a = b.toUInt16

theorem UInt16.toUSize_eq_mod_65536_iff (a : UInt16) (b : USize) : a.toUSize = b % 65536 ↔ a = b.toUInt16

theorem UInt32.toUInt64_eq_mod_4294967296_iff (a : UInt32) (b : UInt64) : a.toUInt64 = b % 4294967296 ↔ a = b.toUInt32

theorem UInt32.toUSize_eq_mod_4294967296_iff (a : UInt32) (b : USize) : a.toUSize = b % 4294967296 ↔ a = b.toUInt32

theorem USize.toUInt64_eq_mod_usizeSize_iff (a : USize) (b : UInt64) : a.toUInt64 = b % UInt64.ofNat size ↔ a = b.toUSize

theorem UInt8.toUInt16_inj {a b : UInt8} : a.toUInt16 = b.toUInt16 ↔ a = b

theorem UInt8.toUInt32_inj {a b : UInt8} : a.toUInt32 = b.toUInt32 ↔ a = b

theorem UInt8.toUInt64_inj {a b : UInt8} : a.toUInt64 = b.toUInt64 ↔ a = b

theorem UInt8.toUSize_inj {a b : UInt8} : a.toUSize = b.toUSize ↔ a = b

theorem UInt16.toUInt32_inj {a b : UInt16} : a.toUInt32 = b.toUInt32 ↔ a = b

theorem UInt16.toUInt64_inj {a b : UInt16} : a.toUInt64 = b.toUInt64 ↔ a = b

theorem UInt16.toUSize_inj {a b : UInt16} : a.toUSize = b.toUSize ↔ a = b

theorem UInt32.toUInt64_inj {a b : UInt32} : a.toUInt64 = b.toUInt64 ↔ a = b

theorem UInt32.toUSize_inj {a b : UInt32} : a.toUSize = b.toUSize ↔ a = b

theorem USize.toUInt64_inj {a b : USize} : a.toUInt64 = b.toUInt64 ↔ a = b

theorem UInt8.lt_iff_toFin_lt {a b : UInt8} : a < b ↔ a.toFin < b.toFin

theorem UInt16.lt_iff_toFin_lt {a b : UInt16} : a < b ↔ a.toFin < b.toFin

theorem UInt32.lt_iff_toFin_lt {a b : UInt32} : a < b ↔ a.toFin < b.toFin

theorem UInt64.lt_iff_toFin_lt {a b : UInt64} : a < b ↔ a.toFin < b.toFin

theorem USize.lt_iff_toFin_lt {a b : USize} : a < b ↔ a.toFin < b.toFin

theorem UInt8.le_iff_toFin_le {a b : UInt8} : a ≤ b ↔ a.toFin ≤ b.toFin

theorem UInt16.le_iff_toFin_le {a b : UInt16} : a ≤ b ↔ a.toFin ≤ b.toFin

theorem UInt32.le_iff_toFin_le {a b : UInt32} : a ≤ b ↔ a.toFin ≤ b.toFin

theorem UInt64.le_iff_toFin_le {a b : UInt64} : a ≤ b ↔ a.toFin ≤ b.toFin

theorem USize.le_iff_toFin_le {a b : USize} : a ≤ b ↔ a.toFin ≤ b.toFin

@[simp]

theorem UInt8.toUInt16_lt {a b : UInt8} : a.toUInt16 < b.toUInt16 ↔ a < b

@[simp]

theorem UInt8.toUInt32_lt {a b : UInt8} : a.toUInt32 < b.toUInt32 ↔ a < b

@[simp]

theorem UInt8.toUInt64_lt {a b : UInt8} : a.toUInt64 < b.toUInt64 ↔ a < b

@[simp]

theorem UInt8.toUSize_lt {a b : UInt8} : a.toUSize < b.toUSize ↔ a < b

@[simp]

theorem UInt16.toUInt32_lt {a b : UInt16} : a.toUInt32 < b.toUInt32 ↔ a < b

@[simp]

theorem UInt16.toUInt64_lt {a b : UInt16} : a.toUInt64 < b.toUInt64 ↔ a < b

@[simp]

theorem UInt16.toUSize_lt {a b : UInt16} : a.toUSize < b.toUSize ↔ a < b

@[simp]

theorem UInt32.toUInt64_lt {a b : UInt32} : a.toUInt64 < b.toUInt64 ↔ a < b

@[simp]

theorem UInt32.toUSize_lt {a b : UInt32} : a.toUSize < b.toUSize ↔ a < b

@[simp]

theorem USize.toUInt64_lt {a b : USize} : a.toUInt64 < b.toUInt64 ↔ a < b

@[simp]

theorem UInt16.toUInt8_lt {a b : UInt16} : a.toUInt8 < b.toUInt8 ↔ a % 256 < b % 256

@[simp]

theorem UInt32.toUInt8_lt {a b : UInt32} : a.toUInt8 < b.toUInt8 ↔ a % 256 < b % 256

@[simp]

theorem UInt64.toUInt8_lt {a b : UInt64} : a.toUInt8 < b.toUInt8 ↔ a % 256 < b % 256

@[simp]

theorem USize.toUInt8_lt {a b : USize} : a.toUInt8 < b.toUInt8 ↔ a % 256 < b % 256

@[simp]

theorem UInt32.toUInt16_lt {a b : UInt32} : a.toUInt16 < b.toUInt16 ↔ a % 65536 < b % 65536

@[simp]

theorem UInt64.toUInt16_lt {a b : UInt64} : a.toUInt16 < b.toUInt16 ↔ a % 65536 < b % 65536

@[simp]

theorem USize.toUInt16_lt {a b : USize} : a.toUInt16 < b.toUInt16 ↔ a % 65536 < b % 65536

@[simp]

theorem UInt64.toUInt32_lt {a b : UInt64} : a.toUInt32 < b.toUInt32 ↔ a % 4294967296 < b % 4294967296

@[simp]

theorem USize.toUInt32_lt {a b : USize} : a.toUInt32 < b.toUInt32 ↔ a % 4294967296 < b % 4294967296

@[simp]

theorem UInt64.toUSize_lt {a b : UInt64} : a.toUSize < b.toUSize ↔ a % ofNat USize.size < b % ofNat USize.size

@[simp]

theorem UInt8.toUInt16_le {a b : UInt8} : a.toUInt16 ≤ b.toUInt16 ↔ a ≤ b

@[simp]

theorem UInt8.toUInt32_le {a b : UInt8} : a.toUInt32 ≤ b.toUInt32 ↔ a ≤ b

@[simp]

theorem UInt8.toUInt64_le {a b : UInt8} : a.toUInt64 ≤ b.toUInt64 ↔ a ≤ b

@[simp]

theorem UInt8.toUSize_le {a b : UInt8} : a.toUSize ≤ b.toUSize ↔ a ≤ b

@[simp]

theorem UInt16.toUInt32_le {a b : UInt16} : a.toUInt32 ≤ b.toUInt32 ↔ a ≤ b

@[simp]

theorem UInt16.toUInt64_le {a b : UInt16} : a.toUInt64 ≤ b.toUInt64 ↔ a ≤ b

@[simp]

theorem UInt16.toUSize_le {a b : UInt16} : a.toUSize ≤ b.toUSize ↔ a ≤ b

@[simp]

theorem UInt32.toUInt64_le {a b : UInt32} : a.toUInt64 ≤ b.toUInt64 ↔ a ≤ b

@[simp]

theorem UInt32.toUSize_le {a b : UInt32} : a.toUSize ≤ b.toUSize ↔ a ≤ b

@[simp]

theorem USize.toUInt64_le {a b : USize} : a.toUInt64 ≤ b.toUInt64 ↔ a ≤ b

@[simp]

theorem UInt16.toUInt8_le {a b : UInt16} : a.toUInt8 ≤ b.toUInt8 ↔ a % 256 ≤ b % 256

@[simp]

theorem UInt32.toUInt8_le {a b : UInt32} : a.toUInt8 ≤ b.toUInt8 ↔ a % 256 ≤ b % 256

@[simp]

theorem UInt64.toUInt8_le {a b : UInt64} : a.toUInt8 ≤ b.toUInt8 ↔ a % 256 ≤ b % 256

@[simp]

theorem USize.toUInt8_le {a b : USize} : a.toUInt8 ≤ b.toUInt8 ↔ a % 256 ≤ b % 256

@[simp]

theorem UInt32.toUInt16_le {a b : UInt32} : a.toUInt16 ≤ b.toUInt16 ↔ a % 65536 ≤ b % 65536

@[simp]

theorem UInt64.toUInt16_le {a b : UInt64} : a.toUInt16 ≤ b.toUInt16 ↔ a % 65536 ≤ b % 65536

@[simp]

theorem USize.toUInt16_le {a b : USize} : a.toUInt16 ≤ b.toUInt16 ↔ a % 65536 ≤ b % 65536

@[simp]

theorem UInt64.toUInt32_le {a b : UInt64} : a.toUInt32 ≤ b.toUInt32 ↔ a % 4294967296 ≤ b % 4294967296

@[simp]

theorem USize.toUInt32_le {a b : USize} : a.toUInt32 ≤ b.toUInt32 ↔ a % 4294967296 ≤ b % 4294967296

@[simp]

theorem UInt64.toUSize_le {a b : UInt64} : a.toUSize ≤ b.toUSize ↔ a % ofNat USize.size ≤ b % ofNat USize.size

@[simp]

theorem UInt16.toUInt8_neg (a : UInt16) : (-a).toUInt8 = -a.toUInt8

@[simp]

theorem UInt32.toUInt8_neg (a : UInt32) : (-a).toUInt8 = -a.toUInt8

@[simp]

theorem UInt32.toUInt16_neg (a : UInt32) : (-a).toUInt16 = -a.toUInt16

@[simp]

theorem UInt64.toUInt8_neg (a : UInt64) : (-a).toUInt8 = -a.toUInt8

@[simp]

theorem UInt64.toUInt16_neg (a : UInt64) : (-a).toUInt16 = -a.toUInt16

@[simp]

theorem UInt64.toUInt32_neg (a : UInt64) : (-a).toUInt32 = -a.toUInt32

@[simp]

theorem UInt64.toUSize_neg (a : UInt64) : (-a).toUSize = -a.toUSize

@[simp]

theorem USize.toUInt8_neg (a : USize) : (-a).toUInt8 = -a.toUInt8

@[simp]

theorem USize.toUInt16_neg (a : USize) : (-a).toUInt16 = -a.toUInt16

@[simp]

theorem USize.toUInt32_neg (a : USize) : (-a).toUInt32 = -a.toUInt32

@[simp]

theorem UInt8.toUInt16_neg (a : UInt8) : (-a).toUInt16 = -a.toUInt16 % 256

@[simp]

theorem UInt8.toUInt32_neg (a : UInt8) : (-a).toUInt32 = -a.toUInt32 % 256

@[simp]

theorem UInt8.toUInt64_neg (a : UInt8) : (-a).toUInt64 = -a.toUInt64 % 256

@[simp]

theorem UInt8.toUSize_neg (a : UInt8) : (-a).toUSize = -a.toUSize % 256

@[simp]

theorem UInt16.toUInt32_neg (a : UInt16) : (-a).toUInt32 = -a.toUInt32 % 65536

@[simp]

theorem UInt16.toUInt64_neg (a : UInt16) : (-a).toUInt64 = -a.toUInt64 % 65536

@[simp]

theorem UInt16.toUSize_neg (a : UInt16) : (-a).toUSize = -a.toUSize % 65536

@[simp]

theorem UInt32.toUInt64_neg (a : UInt32) : (-a).toUInt64 = -a.toUInt64 % 4294967296

@[simp]

theorem UInt32.toUSize_neg (a : UInt32) : (-a).toUSize = -a.toUSize % 4294967296

@[simp]

theorem USize.toUInt64_neg (a : USize) : (-a).toUInt64 = -a.toUInt64 % UInt64.ofNat size

@[simp]

theorem UInt8.toNat_neg (a : UInt8) : (-a).toNat = (size - a.toNat) % size

@[simp]

theorem UInt16.toNat_neg (a : UInt16) : (-a).toNat = (size - a.toNat) % size

@[simp]

theorem UInt32.toNat_neg (a : UInt32) : (-a).toNat = (size - a.toNat) % size

@[simp]

theorem UInt64.toNat_neg (a : UInt64) : (-a).toNat = (size - a.toNat) % size

@[simp]

theorem USize.toNat_neg (a : USize) : (-a).toNat = (size - a.toNat) % size

theorem UInt8.sub_eq_add_neg (a b : UInt8) : a - b = a + -b

theorem UInt16.sub_eq_add_neg (a b : UInt16) : a - b = a + -b

theorem UInt32.sub_eq_add_neg (a b : UInt32) : a - b = a + -b

theorem UInt64.sub_eq_add_neg (a b : UInt64) : a - b = a + -b

theorem USize.sub_eq_add_neg (a b : USize) : a - b = a + -b

theorem UInt8.add_neg_eq_sub {a b : UInt8} : a + -b = a - b

theorem UInt16.add_neg_eq_sub {a b : UInt16} : a + -b = a - b

theorem UInt32.add_neg_eq_sub {a b : UInt32} : a + -b = a - b

theorem UInt64.add_neg_eq_sub {a b : UInt64} : a + -b = a - b

theorem USize.add_neg_eq_sub {a b : USize} : a + -b = a - b

theorem UInt8.neg_one_eq : -1 = 255

theorem UInt16.neg_one_eq : -1 = 65535

theorem UInt32.neg_one_eq : -1 = 4294967295

theorem UInt64.neg_one_eq : -1 = 18446744073709551615

theorem USize.neg_one_eq : -1 = ofNatLT (size - 1) ⋯

theorem UInt8.toBitVec_zero : toBitVec 0 = 0#8

theorem UInt16.toBitVec_zero : toBitVec 0 = 0#16

theorem UInt32.toBitVec_zero : toBitVec 0 = 0#32

theorem UInt64.toBitVec_zero : toBitVec 0 = 0#64

theorem USize.toBitVec_zero : toBitVec 0 = 0#System.Platform.numBits

theorem UInt8.toBitVec_one : toBitVec 1 = 1#8

theorem UInt16.toBitVec_one : toBitVec 1 = 1#16

theorem UInt32.toBitVec_one : toBitVec 1 = 1#32

theorem UInt64.toBitVec_one : toBitVec 1 = 1#64

theorem USize.toBitVec_one : toBitVec 1 = 1#System.Platform.numBits

theorem UInt8.neg_eq_neg_one_mul (a : UInt8) : -a = -1 * a

theorem UInt16.neg_eq_neg_one_mul (a : UInt16) : -a = -1 * a

theorem UInt32.neg_eq_neg_one_mul (a : UInt32) : -a = -1 * a

theorem UInt64.neg_eq_neg_one_mul (a : UInt64) : -a = -1 * a

theorem USize.neg_eq_neg_one_mul (a : USize) : -a = -1 * a

theorem UInt8.sub_eq_add_mul (a b : UInt8) : a - b = a + 255 * b

theorem UInt16.sub_eq_add_mul (a b : UInt16) : a - b = a + 65535 * b

theorem UInt32.sub_eq_add_mul (a b : UInt32) : a - b = a + 4294967295 * b

theorem UInt64.sub_eq_add_mul (a b : UInt64) : a - b = a + 18446744073709551615 * b

theorem USize.sub_eq_add_mul (a b : USize) : a - b = a + ofNatLT (size - 1) ⋯ * b

@[simp]

theorem UInt8.ofNat_usizeSize_sub_one : ofNat (USize.size - 1) = 255

@[simp]

theorem UInt16.ofNat_usizeSize_sub_one : ofNat (USize.size - 1) = 65535

@[simp]

theorem UInt32.ofNat_usizeSize_sub_one : ofNat (USize.size - 1) = 4294967295

@[simp]

theorem USize.ofNat_uInt64Size_sub_one : ofNat (UInt64.size - 1) = ofNatLT (size - 1) ⋯

@[simp]

theorem UInt16.toUInt8_sub (a b : UInt16) : (a - b).toUInt8 = a.toUInt8 - b.toUInt8

@[simp]

theorem UInt32.toUInt8_sub (a b : UInt32) : (a - b).toUInt8 = a.toUInt8 - b.toUInt8

@[simp]

theorem UInt32.toUInt16_sub (a b : UInt32) : (a - b).toUInt16 = a.toUInt16 - b.toUInt16

@[simp]

theorem UInt64.toUInt8_sub (a b : UInt64) : (a - b).toUInt8 = a.toUInt8 - b.toUInt8

@[simp]

theorem UInt64.toUInt16_sub (a b : UInt64) : (a - b).toUInt16 = a.toUInt16 - b.toUInt16

@[simp]

theorem UInt64.toUInt32_sub (a b : UInt64) : (a - b).toUInt32 = a.toUInt32 - b.toUInt32

@[simp]

theorem UInt64.toUSize_sub (a b : UInt64) : (a - b).toUSize = a.toUSize - b.toUSize

@[simp]

theorem USize.toUInt8_sub (a b : USize) : (a - b).toUInt8 = a.toUInt8 - b.toUInt8

@[simp]

theorem USize.toUInt16_sub (a b : USize) : (a - b).toUInt16 = a.toUInt16 - b.toUInt16

@[simp]

theorem USize.toUInt32_sub (a b : USize) : (a - b).toUInt32 = a.toUInt32 - b.toUInt32

@[simp]

theorem UInt8.toUInt16_sub (a b : UInt8) : (a - b).toUInt16 = (a.toUInt16 - b.toUInt16) % 256

@[simp]

theorem UInt8.toUInt32_sub (a b : UInt8) : (a - b).toUInt32 = (a.toUInt32 - b.toUInt32) % 256

@[simp]

theorem UInt8.toUInt64_sub (a b : UInt8) : (a - b).toUInt64 = (a.toUInt64 - b.toUInt64) % 256

@[simp]

theorem UInt8.toUSize_sub (a b : UInt8) : (a - b).toUSize = (a.toUSize - b.toUSize) % 256

@[simp]

theorem UInt16.toUInt32_sub (a b : UInt16) : (a - b).toUInt32 = (a.toUInt32 - b.toUInt32) % 65536

@[simp]

theorem UInt16.toUInt64_sub (a b : UInt16) : (a - b).toUInt64 = (a.toUInt64 - b.toUInt64) % 65536

@[simp]

theorem UInt16.toUSize_sub (a b : UInt16) : (a - b).toUSize = (a.toUSize - b.toUSize) % 65536

@[simp]

theorem UInt32.toUInt64_sub (a b : UInt32) : (a - b).toUInt64 = (a.toUInt64 - b.toUInt64) % 4294967296

@[simp]

theorem UInt32.toUSize_sub (a b : UInt32) : (a - b).toUSize = (a.toUSize - b.toUSize) % 4294967296

@[simp]

theorem USize.toUInt64_sub (a b : USize) : (a - b).toUInt64 = (a.toUInt64 - b.toUInt64) % UInt64.ofNat size

@[simp]

theorem UInt8.ofBitVec_neg (b : BitVec 8) : { toBitVec := -b } = -{ toBitVec := b }

@[simp]

theorem UInt16.ofBitVec_neg (b : BitVec 16) : { toBitVec := -b } = -{ toBitVec := b }

@[simp]

theorem UInt32.ofBitVec_neg (b : BitVec 32) : { toBitVec := -b } = -{ toBitVec := b }

@[simp]

theorem UInt64.ofBitVec_neg (b : BitVec 64) : { toBitVec := -b } = -{ toBitVec := b }

@[simp]

theorem USize.ofBitVec_neg (b : BitVec System.Platform.numBits) : { toBitVec := -b } = -{ toBitVec := b }

@[simp]

theorem UInt8.ofFin_div (a b : Fin size) : ofFin (a / b) = ofFin a / ofFin b

@[simp]

theorem UInt16.ofFin_div (a b : Fin size) : ofFin (a / b) = ofFin a / ofFin b

@[simp]

theorem UInt32.ofFin_div (a b : Fin size) : ofFin (a / b) = ofFin a / ofFin b

@[simp]

theorem UInt64.ofFin_div (a b : Fin size) : ofFin (a / b) = ofFin a / ofFin b

@[simp]

theorem USize.ofFin_div (a b : Fin size) : ofFin (a / b) = ofFin a / ofFin b

@[simp]

theorem UInt8.ofBitVec_div (a b : BitVec 8) : { toBitVec := a / b } = { toBitVec := a } / { toBitVec := b }

@[simp]

theorem UInt16.ofBitVec_div (a b : BitVec 16) : { toBitVec := a / b } = { toBitVec := a } / { toBitVec := b }

@[simp]

theorem UInt32.ofBitVec_div (a b : BitVec 32) : { toBitVec := a / b } = { toBitVec := a } / { toBitVec := b }

@[simp]

theorem UInt64.ofBitVec_div (a b : BitVec 64) : { toBitVec := a / b } = { toBitVec := a } / { toBitVec := b }

@[simp]

theorem USize.ofBitVec_div (a b : BitVec System.Platform.numBits) : { toBitVec := a / b } = { toBitVec := a } / { toBitVec := b }

@[simp]

theorem UInt8.ofFin_mod (a b : Fin size) : ofFin (a % b) = ofFin a % ofFin b

@[simp]

theorem UInt16.ofFin_mod (a b : Fin size) : ofFin (a % b) = ofFin a % ofFin b

@[simp]

theorem UInt32.ofFin_mod (a b : Fin size) : ofFin (a % b) = ofFin a % ofFin b

@[simp]

theorem UInt64.ofFin_mod (a b : Fin size) : ofFin (a % b) = ofFin a % ofFin b

@[simp]

theorem USize.ofFin_mod (a b : Fin size) : ofFin (a % b) = ofFin a % ofFin b

@[simp]

theorem UInt8.ofBitVec_mod (a b : BitVec 8) : { toBitVec := a % b } = { toBitVec := a } % { toBitVec := b }

@[simp]

theorem UInt16.ofBitVec_mod (a b : BitVec 16) : { toBitVec := a % b } = { toBitVec := a } % { toBitVec := b }

@[simp]

theorem UInt32.ofBitVec_mod (a b : BitVec 32) : { toBitVec := a % b } = { toBitVec := a } % { toBitVec := b }

@[simp]

theorem UInt64.ofBitVec_mod (a b : BitVec 64) : { toBitVec := a % b } = { toBitVec := a } % { toBitVec := b }

@[simp]

theorem USize.ofBitVec_mod (a b : BitVec System.Platform.numBits) : { toBitVec := a % b } = { toBitVec := a } % { toBitVec := b }

theorem UInt8.ofNat_eq_iff_mod_eq_toNat (a : Nat) (b : UInt8) : ofNat a = b ↔ a % 2 ^ 8 = b.toNat

theorem UInt16.ofNat_eq_iff_mod_eq_toNat (a : Nat) (b : UInt16) : ofNat a = b ↔ a % 2 ^ 16 = b.toNat

theorem UInt32.ofNat_eq_iff_mod_eq_toNat (a : Nat) (b : UInt32) : ofNat a = b ↔ a % 2 ^ 32 = b.toNat

theorem UInt64.ofNat_eq_iff_mod_eq_toNat (a : Nat) (b : UInt64) : ofNat a = b ↔ a % 2 ^ 64 = b.toNat

theorem USize.ofNat_eq_iff_mod_eq_toNat (a : Nat) (b : USize) : ofNat a = b ↔ a % 2 ^ System.Platform.numBits = b.toNat

@[simp]

theorem UInt8.ofNat_div {a b : Nat} (ha : a < 2 ^ 8) (hb : b < 2 ^ 8) : ofNat (a / b) = ofNat a / ofNat b

@[simp]

theorem UInt16.ofNat_div {a b : Nat} (ha : a < 2 ^ 16) (hb : b < 2 ^ 16) : ofNat (a / b) = ofNat a / ofNat b

@[simp]

theorem UInt32.ofNat_div {a b : Nat} (ha : a < 2 ^ 32) (hb : b < 2 ^ 32) : ofNat (a / b) = ofNat a / ofNat b

@[simp]

theorem UInt64.ofNat_div {a b : Nat} (ha : a < 2 ^ 64) (hb : b < 2 ^ 64) : ofNat (a / b) = ofNat a / ofNat b

@[simp]

theorem USize.ofNat_div {a b : Nat} (ha : a < 2 ^ System.Platform.numBits) (hb : b < 2 ^ System.Platform.numBits) : ofNat (a / b) = ofNat a / ofNat b

@[simp]

theorem UInt8.ofNatLT_div {a b : Nat} (ha : a < 2 ^ 8) (hb : b < 2 ^ 8) : ofNatLT (a / b) ⋯ = ofNatLT a ha / ofNatLT b hb

@[simp]

theorem UInt16.ofNatLT_div {a b : Nat} (ha : a < 2 ^ 16) (hb : b < 2 ^ 16) : ofNatLT (a / b) ⋯ = ofNatLT a ha / ofNatLT b hb

@[simp]

theorem UInt32.ofNatLT_div {a b : Nat} (ha : a < 2 ^ 32) (hb : b < 2 ^ 32) : ofNatLT (a / b) ⋯ = ofNatLT a ha / ofNatLT b hb

@[simp]

theorem UInt64.ofNatLT_div {a b : Nat} (ha : a < 2 ^ 64) (hb : b < 2 ^ 64) : ofNatLT (a / b) ⋯ = ofNatLT a ha / ofNatLT b hb

@[simp]

theorem USize.ofNatLT_div {a b : Nat} (ha : a < 2 ^ System.Platform.numBits) (hb : b < 2 ^ System.Platform.numBits) : ofNatLT (a / b) ⋯ = ofNatLT a ha / ofNatLT b hb

@[simp]

theorem UInt8.ofNat_mod {a b : Nat} (ha : a < 2 ^ 8) (hb : b < 2 ^ 8) : ofNat (a % b) = ofNat a % ofNat b

@[simp]

theorem UInt16.ofNat_mod {a b : Nat} (ha : a < 2 ^ 16) (hb : b < 2 ^ 16) : ofNat (a % b) = ofNat a % ofNat b

@[simp]

theorem UInt32.ofNat_mod {a b : Nat} (ha : a < 2 ^ 32) (hb : b < 2 ^ 32) : ofNat (a % b) = ofNat a % ofNat b

@[simp]

theorem UInt64.ofNat_mod {a b : Nat} (ha : a < 2 ^ 64) (hb : b < 2 ^ 64) : ofNat (a % b) = ofNat a % ofNat b

@[simp]

theorem USize.ofNat_mod {a b : Nat} (ha : a < 2 ^ System.Platform.numBits) (hb : b < 2 ^ System.Platform.numBits) : ofNat (a % b) = ofNat a % ofNat b

@[simp]

theorem UInt8.ofNatLT_mod {a b : Nat} (ha : a < 2 ^ 8) (hb : b < 2 ^ 8) : ofNatLT (a % b) ⋯ = ofNatLT a ha % ofNatLT b hb

@[simp]

theorem UInt16.ofNatLT_mod {a b : Nat} (ha : a < 2 ^ 16) (hb : b < 2 ^ 16) : ofNatLT (a % b) ⋯ = ofNatLT a ha % ofNatLT b hb

@[simp]

theorem UInt32.ofNatLT_mod {a b : Nat} (ha : a < 2 ^ 32) (hb : b < 2 ^ 32) : ofNatLT (a % b) ⋯ = ofNatLT a ha % ofNatLT b hb

@[simp]

theorem UInt64.ofNatLT_mod {a b : Nat} (ha : a < 2 ^ 64) (hb : b < 2 ^ 64) : ofNatLT (a % b) ⋯ = ofNatLT a ha % ofNatLT b hb

@[simp]

theorem USize.ofNatLT_mod {a b : Nat} (ha : a < 2 ^ System.Platform.numBits) (hb : b < 2 ^ System.Platform.numBits) : ofNatLT (a % b) ⋯ = ofNatLT a ha % ofNatLT b hb

@[simp]

theorem UInt8.ofInt_one : ofInt 1 = 1

@[simp]

theorem UInt8.ofInt_neg_one : ofInt (-1) = -1

@[simp]

theorem UInt16.ofInt_one : ofInt 1 = 1

@[simp]

theorem UInt16.ofInt_neg_one : ofInt (-1) = -1

@[simp]

theorem UInt32.ofInt_one : ofInt 1 = 1

@[simp]

theorem UInt32.ofInt_neg_one : ofInt (-1) = -1

@[simp]

theorem UInt64.ofInt_one : ofInt 1 = 1

@[simp]

theorem UInt64.ofInt_neg_one : ofInt (-1) = -1

@[simp]

theorem USize.ofInt_one : ofInt 1 = 1

@[simp]

theorem USize.ofInt_neg_one : ofInt (-1) = -1

@[simp]

theorem UInt8.ofNat_add (a b : Nat) : ofNat (a + b) = ofNat a + ofNat b

@[simp]

theorem UInt16.ofNat_add (a b : Nat) : ofNat (a + b) = ofNat a + ofNat b

@[simp]

theorem UInt32.ofNat_add (a b : Nat) : ofNat (a + b) = ofNat a + ofNat b

@[simp]

theorem UInt64.ofNat_add (a b : Nat) : ofNat (a + b) = ofNat a + ofNat b

@[simp]

theorem USize.ofNat_add (a b : Nat) : ofNat (a + b) = ofNat a + ofNat b

@[simp]

theorem UInt8.ofInt_add (x y : Int) : ofInt (x + y) = ofInt x + ofInt y

@[simp]

theorem UInt16.ofInt_add (x y : Int) : ofInt (x + y) = ofInt x + ofInt y

@[simp]

theorem UInt32.ofInt_add (x y : Int) : ofInt (x + y) = ofInt x + ofInt y

@[simp]

theorem UInt64.ofInt_add (x y : Int) : ofInt (x + y) = ofInt x + ofInt y

theorem System.Platform.two_pow_numBits_nonneg : 0 ≤ 2 ^ numBits

theorem System.Platform.two_pow_numBits_ne_zero : 2 ^ numBits ≠ 0

@[simp]

theorem USize.ofInt_add (x y : Int) : ofInt (x + y) = ofInt x + ofInt y

@[simp]

theorem UInt8.ofNatLT_add {a b : Nat} (hab : a + b < 2 ^ 8) : ofNatLT (a + b) hab = ofNatLT a ⋯ + ofNatLT b ⋯

@[simp]

theorem UInt16.ofNatLT_add {a b : Nat} (hab : a + b < 2 ^ 16) : ofNatLT (a + b) hab = ofNatLT a ⋯ + ofNatLT b ⋯

@[simp]

theorem UInt32.ofNatLT_add {a b : Nat} (hab : a + b < 2 ^ 32) : ofNatLT (a + b) hab = ofNatLT a ⋯ + ofNatLT b ⋯

@[simp]

theorem UInt64.ofNatLT_add {a b : Nat} (hab : a + b < 2 ^ 64) : ofNatLT (a + b) hab = ofNatLT a ⋯ + ofNatLT b ⋯

@[simp]

theorem USize.ofNatLT_add {a b : Nat} (hab : a + b < 2 ^ System.Platform.numBits) : ofNatLT (a + b) hab = ofNatLT a ⋯ + ofNatLT b ⋯

@[simp]

theorem UInt8.ofFin_add (a b : Fin size) : ofFin (a + b) = ofFin a + ofFin b

@[simp]

theorem UInt16.ofFin_add (a b : Fin size) : ofFin (a + b) = ofFin a + ofFin b

@[simp]

theorem UInt32.ofFin_add (a b : Fin size) : ofFin (a + b) = ofFin a + ofFin b

@[simp]

theorem UInt64.ofFin_add (a b : Fin size) : ofFin (a + b) = ofFin a + ofFin b

@[simp]

theorem USize.ofFin_add (a b : Fin size) : ofFin (a + b) = ofFin a + ofFin b

@[simp]

theorem UInt8.ofBitVec_add (a b : BitVec 8) : { toBitVec := a + b } = { toBitVec := a } + { toBitVec := b }

@[simp]

theorem UInt16.ofBitVec_add (a b : BitVec 16) : { toBitVec := a + b } = { toBitVec := a } + { toBitVec := b }

@[simp]

theorem UInt32.ofBitVec_add (a b : BitVec 32) : { toBitVec := a + b } = { toBitVec := a } + { toBitVec := b }

@[simp]

theorem UInt64.ofBitVec_add (a b : BitVec 64) : { toBitVec := a + b } = { toBitVec := a } + { toBitVec := b }

@[simp]

theorem USize.ofBitVec_add (a b : BitVec System.Platform.numBits) : { toBitVec := a + b } = { toBitVec := a } + { toBitVec := b }

@[simp]

theorem UInt8.ofFin_sub (a b : Fin size) : ofFin (a - b) = ofFin a - ofFin b

@[simp]

theorem UInt16.ofFin_sub (a b : Fin size) : ofFin (a - b) = ofFin a - ofFin b

@[simp]

theorem UInt32.ofFin_sub (a b : Fin size) : ofFin (a - b) = ofFin a - ofFin b

@[simp]

theorem UInt64.ofFin_sub (a b : Fin size) : ofFin (a - b) = ofFin a - ofFin b

@[simp]

theorem USize.ofFin_sub (a b : Fin size) : ofFin (a - b) = ofFin a - ofFin b

@[simp]

theorem UInt8.ofBitVec_sub (a b : BitVec 8) : { toBitVec := a - b } = { toBitVec := a } - { toBitVec := b }

@[simp]

theorem UInt16.ofBitVec_sub (a b : BitVec 16) : { toBitVec := a - b } = { toBitVec := a } - { toBitVec := b }

@[simp]

theorem UInt32.ofBitVec_sub (a b : BitVec 32) : { toBitVec := a - b } = { toBitVec := a } - { toBitVec := b }

@[simp]

theorem UInt64.ofBitVec_sub (a b : BitVec 64) : { toBitVec := a - b } = { toBitVec := a } - { toBitVec := b }

@[simp]

theorem USize.ofBitVec_sub (a b : BitVec System.Platform.numBits) : { toBitVec := a - b } = { toBitVec := a } - { toBitVec := b }

@[simp]

theorem UInt8.add_sub_cancel (a b : UInt8) : a + b - b = a

@[simp]

theorem UInt16.add_sub_cancel (a b : UInt16) : a + b - b = a

@[simp]

theorem UInt32.add_sub_cancel (a b : UInt32) : a + b - b = a

@[simp]

theorem UInt64.add_sub_cancel (a b : UInt64) : a + b - b = a

@[simp]

theorem USize.add_sub_cancel (a b : USize) : a + b - b = a

theorem UInt8.ofNat_sub {a b : Nat} (hab : b ≤ a) : ofNat (a - b) = ofNat a - ofNat b

theorem UInt16.ofNat_sub {a b : Nat} (hab : b ≤ a) : ofNat (a - b) = ofNat a - ofNat b

theorem UInt32.ofNat_sub {a b : Nat} (hab : b ≤ a) : ofNat (a - b) = ofNat a - ofNat b

theorem UInt64.ofNat_sub {a b : Nat} (hab : b ≤ a) : ofNat (a - b) = ofNat a - ofNat b

theorem USize.ofNat_sub {a b : Nat} (hab : b ≤ a) : ofNat (a - b) = ofNat a - ofNat b

theorem UInt8.ofNatLT_sub {a b : Nat} (ha : a < 2 ^ 8) (hab : b ≤ a) : ofNatLT (a - b) ⋯ = ofNatLT a ha - ofNatLT b ⋯

theorem UInt16.ofNatLT_sub {a b : Nat} (ha : a < 2 ^ 16) (hab : b ≤ a) : ofNatLT (a - b) ⋯ = ofNatLT a ha - ofNatLT b ⋯

theorem UInt32.ofNatLT_sub {a b : Nat} (ha : a < 2 ^ 32) (hab : b ≤ a) : ofNatLT (a - b) ⋯ = ofNatLT a ha - ofNatLT b ⋯

theorem UInt64.ofNatLT_sub {a b : Nat} (ha : a < 2 ^ 64) (hab : b ≤ a) : ofNatLT (a - b) ⋯ = ofNatLT a ha - ofNatLT b ⋯

theorem USize.ofNatLT_sub {a b : Nat} (ha : a < 2 ^ System.Platform.numBits) (hab : b ≤ a) : ofNatLT (a - b) ⋯ = ofNatLT a ha - ofNatLT b ⋯

@[simp]

theorem UInt8.ofNat_mul (a b : Nat) : ofNat (a * b) = ofNat a * ofNat b

@[simp]

theorem UInt16.ofNat_mul (a b : Nat) : ofNat (a * b) = ofNat a * ofNat b

@[simp]

theorem UInt32.ofNat_mul (a b : Nat) : ofNat (a * b) = ofNat a * ofNat b

@[simp]

theorem UInt64.ofNat_mul (a b : Nat) : ofNat (a * b) = ofNat a * ofNat b

@[simp]

theorem USize.ofNat_mul (a b : Nat) : ofNat (a * b) = ofNat a * ofNat b

@[simp]

theorem UInt8.ofInt_mul (x y : Int) : ofInt (x * y) = ofInt x * ofInt y

@[simp]

theorem UInt16.ofInt_mul (x y : Int) : ofInt (x * y) = ofInt x * ofInt y

@[simp]

theorem UInt32.ofInt_mul (x y : Int) : ofInt (x * y) = ofInt x * ofInt y

@[simp]

theorem UInt64.ofInt_mul (x y : Int) : ofInt (x * y) = ofInt x * ofInt y

@[simp]

theorem USize.ofInt_mul (x y : Int) : ofInt (x * y) = ofInt x * ofInt y

@[simp]

theorem UInt8.ofNatLT_mul {a b : Nat} (ha : a < 2 ^ 8) (hb : b < 2 ^ 8) (hab : a * b < 2 ^ 8) : ofNatLT (a * b) hab = ofNatLT a ha * ofNatLT b hb

@[simp]

theorem UInt16.ofNatLT_mul {a b : Nat} (ha : a < 2 ^ 16) (hb : b < 2 ^ 16) (hab : a * b < 2 ^ 16) : ofNatLT (a * b) hab = ofNatLT a ha * ofNatLT b hb

@[simp]

theorem UInt32.ofNatLT_mul {a b : Nat} (ha : a < 2 ^ 32) (hb : b < 2 ^ 32) (hab : a * b < 2 ^ 32) : ofNatLT (a * b) hab = ofNatLT a ha * ofNatLT b hb

@[simp]

theorem UInt64.ofNatLT_mul {a b : Nat} (ha : a < 2 ^ 64) (hb : b < 2 ^ 64) (hab : a * b < 2 ^ 64) : ofNatLT (a * b) hab = ofNatLT a ha * ofNatLT b hb

@[simp]

theorem USize.ofNatLT_mul {a b : Nat} (ha : a < 2 ^ System.Platform.numBits) (hb : b < 2 ^ System.Platform.numBits) (hab : a * b < 2 ^ System.Platform.numBits) : ofNatLT (a * b) hab = ofNatLT a ha * ofNatLT b hb

@[simp]

theorem UInt8.ofFin_mul (a b : Fin size) : ofFin (a * b) = ofFin a * ofFin b

@[simp]

theorem UInt16.ofFin_mul (a b : Fin size) : ofFin (a * b) = ofFin a * ofFin b

@[simp]

theorem UInt32.ofFin_mul (a b : Fin size) : ofFin (a * b) = ofFin a * ofFin b

@[simp]

theorem UInt64.ofFin_mul (a b : Fin size) : ofFin (a * b) = ofFin a * ofFin b

@[simp]

theorem USize.ofFin_mul (a b : Fin size) : ofFin (a * b) = ofFin a * ofFin b

@[simp]

theorem UInt8.ofBitVec_mul (a b : BitVec 8) : { toBitVec := a * b } = { toBitVec := a } * { toBitVec := b }

@[simp]

theorem UInt16.ofBitVec_mul (a b : BitVec 16) : { toBitVec := a * b } = { toBitVec := a } * { toBitVec := b }

@[simp]

theorem UInt32.ofBitVec_mul (a b : BitVec 32) : { toBitVec := a * b } = { toBitVec := a } * { toBitVec := b }

@[simp]

theorem UInt64.ofBitVec_mul (a b : BitVec 64) : { toBitVec := a * b } = { toBitVec := a } * { toBitVec := b }

@[simp]

theorem USize.ofBitVec_mul (a b : BitVec System.Platform.numBits) : { toBitVec := a * b } = { toBitVec := a } * { toBitVec := b }

theorem UInt8.ofFin_lt_iff_lt {a b : Fin size} : ofFin a < ofFin b ↔ a < b

theorem UInt16.ofFin_lt_iff_lt {a b : Fin size} : ofFin a < ofFin b ↔ a < b

theorem UInt32.ofFin_lt_iff_lt {a b : Fin size} : ofFin a < ofFin b ↔ a < b

theorem UInt64.ofFin_lt_iff_lt {a b : Fin size} : ofFin a < ofFin b ↔ a < b

theorem USize.ofFin_lt_iff_lt {a b : Fin size} : ofFin a < ofFin b ↔ a < b

theorem UInt8.ofFin_le_iff_le {a b : Fin size} : ofFin a ≤ ofFin b ↔ a ≤ b

theorem UInt16.ofFin_le_iff_le {a b : Fin size} : ofFin a ≤ ofFin b ↔ a ≤ b

theorem UInt32.ofFin_le_iff_le {a b : Fin size} : ofFin a ≤ ofFin b ↔ a ≤ b

theorem UInt64.ofFin_le_iff_le {a b : Fin size} : ofFin a ≤ ofFin b ↔ a ≤ b

theorem USize.ofFin_le_iff_le {a b : Fin size} : ofFin a ≤ ofFin b ↔ a ≤ b

theorem UInt8.ofBitVec_lt_iff_lt {a b : BitVec 8} : { toBitVec := a } < { toBitVec := b } ↔ a < b

theorem UInt16.ofBitVec_lt_iff_lt {a b : BitVec 16} : { toBitVec := a } < { toBitVec := b } ↔ a < b

theorem UInt32.ofBitVec_lt_iff_lt {a b : BitVec 32} : { toBitVec := a } < { toBitVec := b } ↔ a < b

theorem UInt64.ofBitVec_lt_iff_lt {a b : BitVec 64} : { toBitVec := a } < { toBitVec := b } ↔ a < b

theorem USize.ofBitVec_lt_iff_lt {a b : BitVec System.Platform.numBits} : { toBitVec := a } < { toBitVec := b } ↔ a < b

theorem UInt8.ofBitVec_le_iff_le {a b : BitVec 8} : { toBitVec := a } ≤ { toBitVec := b } ↔ a ≤ b

theorem UInt16.ofBitVec_le_iff_le {a b : BitVec 16} : { toBitVec := a } ≤ { toBitVec := b } ↔ a ≤ b

theorem UInt32.ofBitVec_le_iff_le {a b : BitVec 32} : { toBitVec := a } ≤ { toBitVec := b } ↔ a ≤ b

theorem UInt64.ofBitVec_le_iff_le {a b : BitVec 64} : { toBitVec := a } ≤ { toBitVec := b } ↔ a ≤ b

theorem USize.ofBitVec_le_iff_le {a b : BitVec System.Platform.numBits} : { toBitVec := a } ≤ { toBitVec := b } ↔ a ≤ b

theorem UInt8.ofNatLT_lt_iff_lt {a b : Nat} (ha : a < size) (hb : b < size) : ofNatLT a ha < ofNatLT b hb ↔ a < b

theorem UInt16.ofNatLT_lt_iff_lt {a b : Nat} (ha : a < size) (hb : b < size) : ofNatLT a ha < ofNatLT b hb ↔ a < b

theorem UInt32.ofNatLT_lt_iff_lt {a b : Nat} (ha : a < size) (hb : b < size) : ofNatLT a ha < ofNatLT b hb ↔ a < b

theorem UInt64.ofNatLT_lt_iff_lt {a b : Nat} (ha : a < size) (hb : b < size) : ofNatLT a ha < ofNatLT b hb ↔ a < b

theorem USize.ofNatLT_lt_iff_lt {a b : Nat} (ha : a < size) (hb : b < size) : ofNatLT a ha < ofNatLT b hb ↔ a < b

theorem UInt8.ofNatLT_le_iff_le {a b : Nat} (ha : a < size) (hb : b < size) : ofNatLT a ha ≤ ofNatLT b hb ↔ a ≤ b

theorem UInt16.ofNatLT_le_iff_le {a b : Nat} (ha : a < size) (hb : b < size) : ofNatLT a ha ≤ ofNatLT b hb ↔ a ≤ b

theorem UInt32.ofNatLT_le_iff_le {a b : Nat} (ha : a < size) (hb : b < size) : ofNatLT a ha ≤ ofNatLT b hb ↔ a ≤ b

theorem UInt64.ofNatLT_le_iff_le {a b : Nat} (ha : a < size) (hb : b < size) : ofNatLT a ha ≤ ofNatLT b hb ↔ a ≤ b

theorem USize.ofNatLT_le_iff_le {a b : Nat} (ha : a < size) (hb : b < size) : ofNatLT a ha ≤ ofNatLT b hb ↔ a ≤ b

theorem UInt8.ofNat_lt_iff_lt {a b : Nat} (ha : a < size) (hb : b < size) : ofNat a < ofNat b ↔ a < b

theorem UInt16.ofNat_lt_iff_lt {a b : Nat} (ha : a < size) (hb : b < size) : ofNat a < ofNat b ↔ a < b

theorem UInt32.ofNat_lt_iff_lt {a b : Nat} (ha : a < size) (hb : b < size) : ofNat a < ofNat b ↔ a < b

theorem UInt64.ofNat_lt_iff_lt {a b : Nat} (ha : a < size) (hb : b < size) : ofNat a < ofNat b ↔ a < b

theorem USize.ofNat_lt_iff_lt {a b : Nat} (ha : a < size) (hb : b < size) : ofNat a < ofNat b ↔ a < b

theorem UInt8.ofNat_le_iff_le {a b : Nat} (ha : a < size) (hb : b < size) : ofNat a ≤ ofNat b ↔ a ≤ b

theorem UInt16.ofNat_le_iff_le {a b : Nat} (ha : a < size) (hb : b < size) : ofNat a ≤ ofNat b ↔ a ≤ b

theorem UInt32.ofNat_le_iff_le {a b : Nat} (ha : a < size) (hb : b < size) : ofNat a ≤ ofNat b ↔ a ≤ b

theorem UInt64.ofNat_le_iff_le {a b : Nat} (ha : a < size) (hb : b < size) : ofNat a ≤ ofNat b ↔ a ≤ b

theorem USize.ofNat_le_iff_le {a b : Nat} (ha : a < size) (hb : b < size) : ofNat a ≤ ofNat b ↔ a ≤ b

theorem UInt8.toNat_one : toNat 1 = 1

theorem UInt16.toNat_one : toNat 1 = 1

theorem UInt32.toNat_one : toNat 1 = 1

theorem UInt64.toNat_one : toNat 1 = 1

theorem USize.toNat_one : toNat 1 = 1

theorem UInt8.zero_lt_one : 0 < 1

theorem UInt16.zero_lt_one : 0 < 1

theorem UInt32.zero_lt_one : 0 < 1

theorem UInt64.zero_lt_one : 0 < 1

theorem USize.zero_lt_one : 0 < 1

theorem UInt8.zero_ne_one : 0 ≠ 1

theorem UInt16.zero_ne_one : 0 ≠ 1

theorem UInt32.zero_ne_one : 0 ≠ 1

theorem UInt64.zero_ne_one : 0 ≠ 1

theorem USize.zero_ne_one : 0 ≠ 1

theorem UInt8.add_assoc (a b c : UInt8) : a + b + c = a + (b + c)

theorem UInt16.add_assoc (a b c : UInt16) : a + b + c = a + (b + c)

theorem UInt32.add_assoc (a b c : UInt32) : a + b + c = a + (b + c)

theorem UInt64.add_assoc (a b c : UInt64) : a + b + c = a + (b + c)

theorem USize.add_assoc (a b c : USize) : a + b + c = a + (b + c)

instance instAssociativeUInt8HAdd : Std.Associative fun (x1 x2 : UInt8) => x1 + x2

instance instAssociativeUInt16HAdd : Std.Associative fun (x1 x2 : UInt16) => x1 + x2

instance instAssociativeUInt32HAdd : Std.Associative fun (x1 x2 : UInt32) => x1 + x2

instance instAssociativeUInt64HAdd : Std.Associative fun (x1 x2 : UInt64) => x1 + x2

instance instAssociativeUSizeHAdd : Std.Associative fun (x1 x2 : USize) => x1 + x2

theorem UInt8.add_comm (a b : UInt8) : a + b = b + a

theorem UInt16.add_comm (a b : UInt16) : a + b = b + a

theorem UInt32.add_comm (a b : UInt32) : a + b = b + a

theorem UInt64.add_comm (a b : UInt64) : a + b = b + a

theorem USize.add_comm (a b : USize) : a + b = b + a

instance instCommutativeUInt8HAdd : Std.Commutative fun (x1 x2 : UInt8) => x1 + x2

instance instCommutativeUInt16HAdd : Std.Commutative fun (x1 x2 : UInt16) => x1 + x2

instance instCommutativeUInt32HAdd : Std.Commutative fun (x1 x2 : UInt32) => x1 + x2

instance instCommutativeUInt64HAdd : Std.Commutative fun (x1 x2 : UInt64) => x1 + x2

instance instCommutativeUSizeHAdd : Std.Commutative fun (x1 x2 : USize) => x1 + x2

@[simp]

theorem UInt8.add_zero (a : UInt8) : a + 0 = a

@[simp]

theorem UInt16.add_zero (a : UInt16) : a + 0 = a

@[simp]

theorem UInt32.add_zero (a : UInt32) : a + 0 = a

@[simp]

theorem UInt64.add_zero (a : UInt64) : a + 0 = a

@[simp]

theorem USize.add_zero (a : USize) : a + 0 = a

@[simp]

theorem UInt8.zero_add (a : UInt8) : 0 + a = a

@[simp]

theorem UInt16.zero_add (a : UInt16) : 0 + a = a

@[simp]

theorem UInt32.zero_add (a : UInt32) : 0 + a = a

@[simp]

theorem UInt64.zero_add (a : UInt64) : 0 + a = a

@[simp]

theorem USize.zero_add (a : USize) : 0 + a = a

instance instLawfulIdentityUInt8HAddOfNat : Std.LawfulIdentity (fun (x1 x2 : UInt8) => x1 + x2) 0

instance instLawfulIdentityUInt16HAddOfNat : Std.LawfulIdentity (fun (x1 x2 : UInt16) => x1 + x2) 0

instance instLawfulIdentityUInt32HAddOfNat : Std.LawfulIdentity (fun (x1 x2 : UInt32) => x1 + x2) 0

instance instLawfulIdentityUInt64HAddOfNat : Std.LawfulIdentity (fun (x1 x2 : UInt64) => x1 + x2) 0

instance instLawfulIdentityUSizeHAddOfNat : Std.LawfulIdentity (fun (x1 x2 : USize) => x1 + x2) 0

@[simp]

theorem UInt8.sub_zero (a : UInt8) : a - 0 = a

@[simp]

theorem UInt16.sub_zero (a : UInt16) : a - 0 = a

@[simp]

theorem UInt32.sub_zero (a : UInt32) : a - 0 = a

@[simp]

theorem UInt64.sub_zero (a : UInt64) : a - 0 = a

@[simp]

theorem USize.sub_zero (a : USize) : a - 0 = a

@[simp]

theorem UInt8.zero_sub (a : UInt8) : 0 - a = -a

@[simp]

theorem UInt16.zero_sub (a : UInt16) : 0 - a = -a

@[simp]

theorem UInt32.zero_sub (a : UInt32) : 0 - a = -a

@[simp]

theorem UInt64.zero_sub (a : UInt64) : 0 - a = -a

@[simp]

theorem USize.zero_sub (a : USize) : 0 - a = -a

@[simp]

theorem UInt8.sub_self (a : UInt8) : a - a = 0

@[simp]

theorem UInt16.sub_self (a : UInt16) : a - a = 0

@[simp]

theorem UInt32.sub_self (a : UInt32) : a - a = 0

@[simp]

theorem UInt64.sub_self (a : UInt64) : a - a = 0

@[simp]

theorem USize.sub_self (a : USize) : a - a = 0

theorem UInt8.add_left_neg (a : UInt8) : -a + a = 0

theorem UInt8.add_right_neg (a : UInt8) : a + -a = 0

theorem UInt16.add_left_neg (a : UInt16) : -a + a = 0

theorem UInt16.add_right_neg (a : UInt16) : a + -a = 0

theorem UInt32.add_left_neg (a : UInt32) : -a + a = 0

theorem UInt32.add_right_neg (a : UInt32) : a + -a = 0

theorem UInt64.add_left_neg (a : UInt64) : -a + a = 0

theorem UInt64.add_right_neg (a : UInt64) : a + -a = 0

theorem USize.add_left_neg (a : USize) : -a + a = 0

theorem USize.add_right_neg (a : USize) : a + -a = 0

@[simp]

theorem UInt8.neg_zero : -0 = 0

@[simp]

theorem UInt16.neg_zero : -0 = 0

@[simp]

theorem UInt32.neg_zero : -0 = 0

@[simp]

theorem UInt64.neg_zero : -0 = 0

@[simp]

theorem USize.neg_zero : -0 = 0

@[simp]

theorem UInt8.sub_add_cancel (a b : UInt8) : a - b + b = a

@[simp]

theorem UInt16.sub_add_cancel (a b : UInt16) : a - b + b = a

@[simp]

theorem UInt32.sub_add_cancel (a b : UInt32) : a - b + b = a

@[simp]

theorem UInt64.sub_add_cancel (a b : UInt64) : a - b + b = a

@[simp]

theorem USize.sub_add_cancel (a b : USize) : a - b + b = a

theorem UInt8.eq_sub_iff_add_eq {a b c : UInt8} : a = c - b ↔ a + b = c

theorem UInt16.eq_sub_iff_add_eq {a b c : UInt16} : a = c - b ↔ a + b = c

theorem UInt32.eq_sub_iff_add_eq {a b c : UInt32} : a = c - b ↔ a + b = c

theorem UInt64.eq_sub_iff_add_eq {a b c : UInt64} : a = c - b ↔ a + b = c

theorem USize.eq_sub_iff_add_eq {a b c : USize} : a = c - b ↔ a + b = c

theorem UInt8.sub_eq_iff_eq_add {a b c : UInt8} : a - b = c ↔ a = c + b

theorem UInt16.sub_eq_iff_eq_add {a b c : UInt16} : a - b = c ↔ a = c + b

theorem UInt32.sub_eq_iff_eq_add {a b c : UInt32} : a - b = c ↔ a = c + b

theorem UInt64.sub_eq_iff_eq_add {a b c : UInt64} : a - b = c ↔ a = c + b

theorem USize.sub_eq_iff_eq_add {a b c : USize} : a - b = c ↔ a = c + b

@[simp]

theorem UInt8.neg_neg {a : UInt8} : - -a = a

@[simp]

theorem UInt16.neg_neg {a : UInt16} : - -a = a

@[simp]

theorem UInt32.neg_neg {a : UInt32} : - -a = a

@[simp]

theorem UInt64.neg_neg {a : UInt64} : - -a = a

@[simp]

theorem USize.neg_neg {a : USize} : - -a = a

@[simp]

theorem UInt8.neg_inj {a b : UInt8} : -a = -b ↔ a = b

@[simp]

theorem UInt16.neg_inj {a b : UInt16} : -a = -b ↔ a = b

@[simp]

theorem UInt32.neg_inj {a b : UInt32} : -a = -b ↔ a = b

@[simp]

theorem UInt64.neg_inj {a b : UInt64} : -a = -b ↔ a = b

@[simp]

theorem USize.neg_inj {a b : USize} : -a = -b ↔ a = b

@[simp]

theorem UInt8.neg_ne_zero {a : UInt8} : -a ≠ 0 ↔ a ≠ 0

@[simp]

theorem UInt16.neg_ne_zero {a : UInt16} : -a ≠ 0 ↔ a ≠ 0

@[simp]

theorem UInt32.neg_ne_zero {a : UInt32} : -a ≠ 0 ↔ a ≠ 0

@[simp]

theorem UInt64.neg_ne_zero {a : UInt64} : -a ≠ 0 ↔ a ≠ 0

@[simp]

theorem USize.neg_ne_zero {a : USize} : -a ≠ 0 ↔ a ≠ 0

theorem UInt8.neg_add {a b : UInt8} : -(a + b) = -a - b

theorem UInt16.neg_add {a b : UInt16} : -(a + b) = -a - b

theorem UInt32.neg_add {a b : UInt32} : -(a + b) = -a - b

theorem UInt64.neg_add {a b : UInt64} : -(a + b) = -a - b

theorem USize.neg_add {a b : USize} : -(a + b) = -a - b

@[simp]

theorem UInt8.sub_neg {a b : UInt8} : a - -b = a + b

@[simp]

theorem UInt16.sub_neg {a b : UInt16} : a - -b = a + b

@[simp]

theorem UInt32.sub_neg {a b : UInt32} : a - -b = a + b

@[simp]

theorem UInt64.sub_neg {a b : UInt64} : a - -b = a + b

@[simp]

theorem USize.sub_neg {a b : USize} : a - -b = a + b

@[simp]

theorem UInt8.neg_sub {a b : UInt8} : -(a - b) = b - a

@[simp]

theorem UInt16.neg_sub {a b : UInt16} : -(a - b) = b - a

@[simp]

theorem UInt32.neg_sub {a b : UInt32} : -(a - b) = b - a

@[simp]

theorem UInt64.neg_sub {a b : UInt64} : -(a - b) = b - a

@[simp]

theorem USize.neg_sub {a b : USize} : -(a - b) = b - a

@[simp]

theorem UInt8.ofInt_neg (x : Int) : ofInt (-x) = -ofInt x

@[simp]

theorem UInt16.ofInt_neg (x : Int) : ofInt (-x) = -ofInt x

@[simp]

theorem UInt32.ofInt_neg (x : Int) : ofInt (-x) = -ofInt x

@[simp]

theorem UInt64.ofInt_neg (x : Int) : ofInt (-x) = -ofInt x

@[simp]

theorem USize.ofInt_neg (x : Int) : ofInt (-x) = -ofInt x

@[simp]

theorem UInt8.add_left_inj {a b : UInt8} (c : UInt8) : a + c = b + c ↔ a = b

@[simp]

theorem UInt16.add_left_inj {a b : UInt16} (c : UInt16) : a + c = b + c ↔ a = b

@[simp]

theorem UInt32.add_left_inj {a b : UInt32} (c : UInt32) : a + c = b + c ↔ a = b

@[simp]

theorem UInt64.add_left_inj {a b : UInt64} (c : UInt64) : a + c = b + c ↔ a = b

@[simp]

theorem USize.add_left_inj {a b : USize} (c : USize) : a + c = b + c ↔ a = b

@[simp]

theorem UInt8.add_right_inj {a b : UInt8} (c : UInt8) : c + a = c + b ↔ a = b

@[simp]

theorem UInt16.add_right_inj {a b : UInt16} (c : UInt16) : c + a = c + b ↔ a = b

@[simp]

theorem UInt32.add_right_inj {a b : UInt32} (c : UInt32) : c + a = c + b ↔ a = b

@[simp]

theorem UInt64.add_right_inj {a b : UInt64} (c : UInt64) : c + a = c + b ↔ a = b

@[simp]

theorem USize.add_right_inj {a b : USize} (c : USize) : c + a = c + b ↔ a = b

@[simp]

theorem UInt8.sub_left_inj {a b : UInt8} (c : UInt8) : a - c = b - c ↔ a = b

@[simp]

theorem UInt16.sub_left_inj {a b : UInt16} (c : UInt16) : a - c = b - c ↔ a = b

@[simp]

theorem UInt32.sub_left_inj {a b : UInt32} (c : UInt32) : a - c = b - c ↔ a = b

@[simp]

theorem UInt64.sub_left_inj {a b : UInt64} (c : UInt64) : a - c = b - c ↔ a = b

@[simp]

theorem USize.sub_left_inj {a b : USize} (c : USize) : a - c = b - c ↔ a = b

@[simp]

theorem UInt8.sub_right_inj {a b : UInt8} (c : UInt8) : c - a = c - b ↔ a = b

@[simp]

theorem UInt16.sub_right_inj {a b : UInt16} (c : UInt16) : c - a = c - b ↔ a = b

@[simp]

theorem UInt32.sub_right_inj {a b : UInt32} (c : UInt32) : c - a = c - b ↔ a = b

@[simp]

theorem UInt64.sub_right_inj {a b : UInt64} (c : UInt64) : c - a = c - b ↔ a = b

@[simp]

theorem USize.sub_right_inj {a b : USize} (c : USize) : c - a = c - b ↔ a = b

@[simp]

theorem UInt8.add_eq_right {a b : UInt8} : a + b = b ↔ a = 0

@[simp]

theorem UInt16.add_eq_right {a b : UInt16} : a + b = b ↔ a = 0

@[simp]

theorem UInt32.add_eq_right {a b : UInt32} : a + b = b ↔ a = 0

@[simp]

theorem UInt64.add_eq_right {a b : UInt64} : a + b = b ↔ a = 0

@[simp]

theorem USize.add_eq_right {a b : USize} : a + b = b ↔ a = 0

@[simp]

theorem UInt8.add_eq_left {a b : UInt8} : a + b = a ↔ b = 0

@[simp]

theorem UInt16.add_eq_left {a b : UInt16} : a + b = a ↔ b = 0

@[simp]

theorem UInt32.add_eq_left {a b : UInt32} : a + b = a ↔ b = 0

@[simp]

theorem UInt64.add_eq_left {a b : UInt64} : a + b = a ↔ b = 0

@[simp]

theorem USize.add_eq_left {a b : USize} : a + b = a ↔ b = 0

@[simp]

theorem UInt8.right_eq_add {a b : UInt8} : b = a + b ↔ a = 0

@[simp]

theorem UInt16.right_eq_add {a b : UInt16} : b = a + b ↔ a = 0

@[simp]

theorem UInt32.right_eq_add {a b : UInt32} : b = a + b ↔ a = 0

@[simp]

theorem UInt64.right_eq_add {a b : UInt64} : b = a + b ↔ a = 0

@[simp]

theorem USize.right_eq_add {a b : USize} : b = a + b ↔ a = 0

@[simp]

theorem UInt8.left_eq_add {a b : UInt8} : a = a + b ↔ b = 0

@[simp]

theorem UInt16.left_eq_add {a b : UInt16} : a = a + b ↔ b = 0

@[simp]

theorem UInt32.left_eq_add {a b : UInt32} : a = a + b ↔ b = 0

@[simp]

theorem UInt64.left_eq_add {a b : UInt64} : a = a + b ↔ b = 0

@[simp]

theorem USize.left_eq_add {a b : USize} : a = a + b ↔ b = 0

theorem UInt8.mul_comm (a b : UInt8) : a * b = b * a

theorem UInt16.mul_comm (a b : UInt16) : a * b = b * a

theorem UInt32.mul_comm (a b : UInt32) : a * b = b * a

theorem UInt64.mul_comm (a b : UInt64) : a * b = b * a

theorem USize.mul_comm (a b : USize) : a * b = b * a

instance instCommutativeUInt8HMul : Std.Commutative fun (x1 x2 : UInt8) => x1 * x2

instance instCommutativeUInt16HMul : Std.Commutative fun (x1 x2 : UInt16) => x1 * x2

instance instCommutativeUInt32HMul : Std.Commutative fun (x1 x2 : UInt32) => x1 * x2

instance instCommutativeUInt64HMul : Std.Commutative fun (x1 x2 : UInt64) => x1 * x2

instance instCommutativeUSizeHMul : Std.Commutative fun (x1 x2 : USize) => x1 * x2

theorem UInt8.mul_assoc (a b c : UInt8) : a * b * c = a * (b * c)

theorem UInt16.mul_assoc (a b c : UInt16) : a * b * c = a * (b * c)

theorem UInt32.mul_assoc (a b c : UInt32) : a * b * c = a * (b * c)

theorem UInt64.mul_assoc (a b c : UInt64) : a * b * c = a * (b * c)

theorem USize.mul_assoc (a b c : USize) : a * b * c = a * (b * c)

instance instAssociativeUInt8HMul : Std.Associative fun (x1 x2 : UInt8) => x1 * x2

instance instAssociativeUInt16HMul : Std.Associative fun (x1 x2 : UInt16) => x1 * x2

instance instAssociativeUInt32HMul : Std.Associative fun (x1 x2 : UInt32) => x1 * x2

instance instAssociativeUInt64HMul : Std.Associative fun (x1 x2 : UInt64) => x1 * x2

instance instAssociativeUSizeHMul : Std.Associative fun (x1 x2 : USize) => x1 * x2

@[simp]

theorem UInt8.mul_one (a : UInt8) : a * 1 = a

@[simp]

theorem UInt16.mul_one (a : UInt16) : a * 1 = a

@[simp]

theorem UInt32.mul_one (a : UInt32) : a * 1 = a

@[simp]

theorem UInt64.mul_one (a : UInt64) : a * 1 = a

@[simp]

theorem USize.mul_one (a : USize) : a * 1 = a

@[simp]

theorem UInt8.one_mul (a : UInt8) : 1 * a = a

@[simp]

theorem UInt16.one_mul (a : UInt16) : 1 * a = a

@[simp]

theorem UInt32.one_mul (a : UInt32) : 1 * a = a

@[simp]

theorem UInt64.one_mul (a : UInt64) : 1 * a = a

@[simp]

theorem USize.one_mul (a : USize) : 1 * a = a

instance instLawfulCommIdentityUInt8HMulOfNat : Std.LawfulCommIdentity (fun (x1 x2 : UInt8) => x1 * x2) 1

instance instLawfulCommIdentityUInt16HMulOfNat : Std.LawfulCommIdentity (fun (x1 x2 : UInt16) => x1 * x2) 1

instance instLawfulCommIdentityUInt32HMulOfNat : Std.LawfulCommIdentity (fun (x1 x2 : UInt32) => x1 * x2) 1

instance instLawfulCommIdentityUInt64HMulOfNat : Std.LawfulCommIdentity (fun (x1 x2 : UInt64) => x1 * x2) 1

instance instLawfulCommIdentityUSizeHMulOfNat : Std.LawfulCommIdentity (fun (x1 x2 : USize) => x1 * x2) 1

@[simp]

theorem UInt8.mul_zero {a : UInt8} : a * 0 = 0

@[simp]

theorem UInt16.mul_zero {a : UInt16} : a * 0 = 0

@[simp]

theorem UInt32.mul_zero {a : UInt32} : a * 0 = 0

@[simp]

theorem UInt64.mul_zero {a : UInt64} : a * 0 = 0

@[simp]

theorem USize.mul_zero {a : USize} : a * 0 = 0

@[simp]

theorem UInt8.zero_mul {a : UInt8} : 0 * a = 0

@[simp]

theorem UInt16.zero_mul {a : UInt16} : 0 * a = 0

@[simp]

theorem UInt32.zero_mul {a : UInt32} : 0 * a = 0

@[simp]

theorem UInt64.zero_mul {a : UInt64} : 0 * a = 0

@[simp]

theorem USize.zero_mul {a : USize} : 0 * a = 0

@[simp]

theorem UInt8.pow_zero (x : UInt8) : x ^ 0 = 1

theorem UInt8.pow_succ (x : UInt8) (n : Nat) : x ^ (n + 1) = x ^ n * x

@[simp]

theorem UInt16.pow_zero (x : UInt16) : x ^ 0 = 1

theorem UInt16.pow_succ (x : UInt16) (n : Nat) : x ^ (n + 1) = x ^ n * x

@[simp]

theorem UInt32.pow_zero (x : UInt32) : x ^ 0 = 1

theorem UInt32.pow_succ (x : UInt32) (n : Nat) : x ^ (n + 1) = x ^ n * x

@[simp]

theorem UInt64.pow_zero (x : UInt64) : x ^ 0 = 1

theorem UInt64.pow_succ (x : UInt64) (n : Nat) : x ^ (n + 1) = x ^ n * x

@[simp]

theorem USize.pow_zero (x : USize) : x ^ 0 = 1

theorem USize.pow_succ (x : USize) (n : Nat) : x ^ (n + 1) = x ^ n * x

@[simp]

theorem UInt8.toBitVec_pow (a : UInt8) (n : Nat) : (a ^ n).toBitVec = a.toBitVec ^ n

@[simp]

theorem UInt16.toBitVec_pow (a : UInt16) (n : Nat) : (a ^ n).toBitVec = a.toBitVec ^ n

@[simp]

theorem UInt32.toBitVec_pow (a : UInt32) (n : Nat) : (a ^ n).toBitVec = a.toBitVec ^ n

@[simp]

theorem UInt64.toBitVec_pow (a : UInt64) (n : Nat) : (a ^ n).toBitVec = a.toBitVec ^ n

@[simp]

theorem USize.toBitVec_pow (a : USize) (n : Nat) : (a ^ n).toBitVec = a.toBitVec ^ n

@[simp]

theorem UInt8.ofBitVec_pow (a : BitVec 8) (n : Nat) : { toBitVec := a ^ n } = { toBitVec := a } ^ n

@[simp]

theorem UInt16.ofBitVec_pow (a : BitVec 16) (n : Nat) : { toBitVec := a ^ n } = { toBitVec := a } ^ n

@[simp]

theorem UInt32.ofBitVec_pow (a : BitVec 32) (n : Nat) : { toBitVec := a ^ n } = { toBitVec := a } ^ n

@[simp]

theorem UInt64.ofBitVec_pow (a : BitVec 64) (n : Nat) : { toBitVec := a ^ n } = { toBitVec := a } ^ n

@[simp]

theorem USize.ofBitVec_pow (a : BitVec System.Platform.numBits) (n : Nat) : { toBitVec := a ^ n } = { toBitVec := a } ^ n

theorem UInt8.mul_add {a b c : UInt8} : a * (b + c) = a * b + a * c

theorem UInt16.mul_add {a b c : UInt16} : a * (b + c) = a * b + a * c

theorem UInt32.mul_add {a b c : UInt32} : a * (b + c) = a * b + a * c

theorem UInt64.mul_add {a b c : UInt64} : a * (b + c) = a * b + a * c

theorem USize.mul_add {a b c : USize} : a * (b + c) = a * b + a * c

theorem UInt8.add_mul {a b c : UInt8} : (a + b) * c = a * c + b * c

theorem UInt16.add_mul {a b c : UInt16} : (a + b) * c = a * c + b * c

theorem UInt32.add_mul {a b c : UInt32} : (a + b) * c = a * c + b * c

theorem UInt64.add_mul {a b c : UInt64} : (a + b) * c = a * c + b * c

theorem USize.add_mul {a b c : USize} : (a + b) * c = a * c + b * c

theorem UInt8.mul_succ {a b : UInt8} : a * (b + 1) = a * b + a

theorem UInt16.mul_succ {a b : UInt16} : a * (b + 1) = a * b + a

theorem UInt32.mul_succ {a b : UInt32} : a * (b + 1) = a * b + a

theorem UInt64.mul_succ {a b : UInt64} : a * (b + 1) = a * b + a

theorem USize.mul_succ {a b : USize} : a * (b + 1) = a * b + a

theorem UInt8.succ_mul {a b : UInt8} : (a + 1) * b = a * b + b

theorem UInt16.succ_mul {a b : UInt16} : (a + 1) * b = a * b + b

theorem UInt32.succ_mul {a b : UInt32} : (a + 1) * b = a * b + b

theorem UInt64.succ_mul {a b : UInt64} : (a + 1) * b = a * b + b

theorem USize.succ_mul {a b : USize} : (a + 1) * b = a * b + b

theorem UInt8.two_mul {a : UInt8} : 2 * a = a + a

theorem UInt16.two_mul {a : UInt16} : 2 * a = a + a

theorem UInt32.two_mul {a : UInt32} : 2 * a = a + a

theorem UInt64.two_mul {a : UInt64} : 2 * a = a + a

theorem USize.two_mul {a : USize} : 2 * a = a + a

theorem UInt8.mul_two {a : UInt8} : a * 2 = a + a

theorem UInt16.mul_two {a : UInt16} : a * 2 = a + a

theorem UInt32.mul_two {a : UInt32} : a * 2 = a + a

theorem UInt64.mul_two {a : UInt64} : a * 2 = a + a

theorem USize.mul_two {a : USize} : a * 2 = a + a

theorem UInt8.neg_mul (a b : UInt8) : -a * b = -(a * b)

theorem UInt16.neg_mul (a b : UInt16) : -a * b = -(a * b)

theorem UInt32.neg_mul (a b : UInt32) : -a * b = -(a * b)

theorem UInt64.neg_mul (a b : UInt64) : -a * b = -(a * b)

theorem USize.neg_mul (a b : USize) : -a * b = -(a * b)

theorem UInt8.mul_neg (a b : UInt8) : a * -b = -(a * b)

theorem UInt16.mul_neg (a b : UInt16) : a * -b = -(a * b)

theorem UInt32.mul_neg (a b : UInt32) : a * -b = -(a * b)

theorem UInt64.mul_neg (a b : UInt64) : a * -b = -(a * b)

theorem USize.mul_neg (a b : USize) : a * -b = -(a * b)

theorem UInt8.neg_mul_neg (a b : UInt8) : -a * -b = a * b

theorem UInt16.neg_mul_neg (a b : UInt16) : -a * -b = a * b

theorem UInt32.neg_mul_neg (a b : UInt32) : -a * -b = a * b

theorem UInt64.neg_mul_neg (a b : UInt64) : -a * -b = a * b

theorem USize.neg_mul_neg (a b : USize) : -a * -b = a * b

theorem UInt8.neg_mul_comm (a b : UInt8) : -a * b = a * -b

theorem UInt16.neg_mul_comm (a b : UInt16) : -a * b = a * -b

theorem UInt32.neg_mul_comm (a b : UInt32) : -a * b = a * -b

theorem UInt64.neg_mul_comm (a b : UInt64) : -a * b = a * -b

theorem USize.neg_mul_comm (a b : USize) : -a * b = a * -b

theorem UInt8.mul_sub {a b c : UInt8} : a * (b - c) = a * b - a * c

theorem UInt16.mul_sub {a b c : UInt16} : a * (b - c) = a * b - a * c

theorem UInt32.mul_sub {a b c : UInt32} : a * (b - c) = a * b - a * c

theorem UInt64.mul_sub {a b c : UInt64} : a * (b - c) = a * b - a * c

theorem USize.mul_sub {a b c : USize} : a * (b - c) = a * b - a * c

theorem UInt8.sub_mul {a b c : UInt8} : (a - b) * c = a * c - b * c

theorem UInt16.sub_mul {a b c : UInt16} : (a - b) * c = a * c - b * c

theorem UInt32.sub_mul {a b c : UInt32} : (a - b) * c = a * c - b * c

theorem UInt64.sub_mul {a b c : UInt64} : (a - b) * c = a * c - b * c

theorem USize.sub_mul {a b c : USize} : (a - b) * c = a * c - b * c

theorem UInt8.neg_add_mul_eq_mul_not {a b : UInt8} : -(a + a * b) = a * ~~~b

theorem UInt16.neg_add_mul_eq_mul_not {a b : UInt16} : -(a + a * b) = a * ~~~b

theorem UInt32.neg_add_mul_eq_mul_not {a b : UInt32} : -(a + a * b) = a * ~~~b

theorem UInt64.neg_add_mul_eq_mul_not {a b : UInt64} : -(a + a * b) = a * ~~~b

theorem USize.neg_add_mul_eq_mul_not {a b : USize} : -(a + a * b) = a * ~~~b

theorem UInt8.neg_mul_not_eq_add_mul {a b : UInt8} : -(a * ~~~b) = a + a * b

theorem UInt16.neg_mul_not_eq_add_mul {a b : UInt16} : -(a * ~~~b) = a + a * b

theorem UInt32.neg_mul_not_eq_add_mul {a b : UInt32} : -(a * ~~~b) = a + a * b

theorem UInt64.neg_mul_not_eq_add_mul {a b : UInt64} : -(a * ~~~b) = a + a * b

theorem USize.neg_mul_not_eq_add_mul {a b : USize} : -(a * ~~~b) = a + a * b

theorem UInt8.le_of_lt {a b : UInt8} : a < b → a ≤ b

theorem UInt16.le_of_lt {a b : UInt16} : a < b → a ≤ b

theorem UInt32.le_of_lt {a b : UInt32} : a < b → a ≤ b

theorem UInt64.le_of_lt {a b : UInt64} : a < b → a ≤ b

theorem USize.le_of_lt {a b : USize} : a < b → a ≤ b

theorem UInt8.lt_of_le_of_ne {a b : UInt8} : a ≤ b → a ≠ b → a < b

theorem UInt16.lt_of_le_of_ne {a b : UInt16} : a ≤ b → a ≠ b → a < b

theorem UInt32.lt_of_le_of_ne {a b : UInt32} : a ≤ b → a ≠ b → a < b

theorem UInt64.lt_of_le_of_ne {a b : UInt64} : a ≤ b → a ≠ b → a < b

theorem USize.lt_of_le_of_ne {a b : USize} : a ≤ b → a ≠ b → a < b

theorem UInt8.lt_iff_le_and_ne {a b : UInt8} : a < b ↔ a ≤ b ∧ a ≠ b

theorem UInt16.lt_iff_le_and_ne {a b : UInt16} : a < b ↔ a ≤ b ∧ a ≠ b

theorem UInt32.lt_iff_le_and_ne {a b : UInt32} : a < b ↔ a ≤ b ∧ a ≠ b

theorem UInt64.lt_iff_le_and_ne {a b : UInt64} : a < b ↔ a ≤ b ∧ a ≠ b

theorem USize.lt_iff_le_and_ne {a b : USize} : a < b ↔ a ≤ b ∧ a ≠ b

@[simp]

theorem UInt8.not_lt_zero {a : UInt8} : ¬a < 0

@[simp]

theorem UInt16.not_lt_zero {a : UInt16} : ¬a < 0

@[simp]

theorem UInt32.not_lt_zero {a : UInt32} : ¬a < 0

@[simp]

theorem UInt64.not_lt_zero {a : UInt64} : ¬a < 0

@[simp]

theorem USize.not_lt_zero {a : USize} : ¬a < 0

@[simp]

theorem UInt8.zero_le {a : UInt8} : 0 ≤ a

@[simp]

theorem UInt16.zero_le {a : UInt16} : 0 ≤ a

@[simp]

theorem UInt32.zero_le {a : UInt32} : 0 ≤ a

@[simp]

theorem UInt64.zero_le {a : UInt64} : 0 ≤ a

@[simp]

theorem USize.zero_le {a : USize} : 0 ≤ a

@[simp]

theorem UInt8.le_zero_iff {a : UInt8} : a ≤ 0 ↔ a = 0

@[simp]

theorem UInt16.le_zero_iff {a : UInt16} : a ≤ 0 ↔ a = 0

@[simp]

theorem UInt32.le_zero_iff {a : UInt32} : a ≤ 0 ↔ a = 0

@[simp]

theorem UInt64.le_zero_iff {a : UInt64} : a ≤ 0 ↔ a = 0

@[simp]

theorem USize.le_zero_iff {a : USize} : a ≤ 0 ↔ a = 0

@[simp]

theorem UInt8.lt_one_iff {a : UInt8} : a < 1 ↔ a = 0

@[simp]

theorem UInt16.lt_one_iff {a : UInt16} : a < 1 ↔ a = 0

@[simp]

theorem UInt32.lt_one_iff {a : UInt32} : a < 1 ↔ a = 0

@[simp]

theorem UInt64.lt_one_iff {a : UInt64} : a < 1 ↔ a = 0

@[simp]

theorem USize.lt_one_iff {a : USize} : a < 1 ↔ a = 0

@[simp]

theorem UInt8.zero_div {a : UInt8} : 0 / a = 0

@[simp]

theorem UInt16.zero_div {a : UInt16} : 0 / a = 0

@[simp]

theorem UInt32.zero_div {a : UInt32} : 0 / a = 0

@[simp]

theorem UInt64.zero_div {a : UInt64} : 0 / a = 0

@[simp]

theorem USize.zero_div {a : USize} : 0 / a = 0

@[simp]

theorem UInt8.div_zero {a : UInt8} : a / 0 = 0

@[simp]

theorem UInt16.div_zero {a : UInt16} : a / 0 = 0

@[simp]

theorem UInt32.div_zero {a : UInt32} : a / 0 = 0

@[simp]

theorem UInt64.div_zero {a : UInt64} : a / 0 = 0

@[simp]

theorem USize.div_zero {a : USize} : a / 0 = 0

@[simp]

theorem UInt8.div_one {a : UInt8} : a / 1 = a

@[simp]

theorem UInt16.div_one {a : UInt16} : a / 1 = a

@[simp]

theorem UInt32.div_one {a : UInt32} : a / 1 = a

@[simp]

theorem UInt64.div_one {a : UInt64} : a / 1 = a

@[simp]

theorem USize.div_one {a : USize} : a / 1 = a

theorem UInt8.div_self {a : UInt8} : a / a = if a = 0 then 0 else 1

theorem UInt16.div_self {a : UInt16} : a / a = if a = 0 then 0 else 1

theorem UInt32.div_self {a : UInt32} : a / a = if a = 0 then 0 else 1

theorem UInt64.div_self {a : UInt64} : a / a = if a = 0 then 0 else 1

theorem USize.div_self {a : USize} : a / a = if a = 0 then 0 else 1

@[simp]

theorem UInt8.mod_zero {a : UInt8} : a % 0 = a

@[simp]

theorem UInt16.mod_zero {a : UInt16} : a % 0 = a

@[simp]

theorem UInt32.mod_zero {a : UInt32} : a % 0 = a

@[simp]

theorem UInt64.mod_zero {a : UInt64} : a % 0 = a

@[simp]

theorem USize.mod_zero {a : USize} : a % 0 = a

@[simp]

theorem UInt8.zero_mod {a : UInt8} : 0 % a = 0

@[simp]

theorem UInt16.zero_mod {a : UInt16} : 0 % a = 0

@[simp]

theorem UInt32.zero_mod {a : UInt32} : 0 % a = 0

@[simp]

theorem UInt64.zero_mod {a : UInt64} : 0 % a = 0

@[simp]

theorem USize.zero_mod {a : USize} : 0 % a = 0

@[simp]

theorem UInt8.mod_one {a : UInt8} : a % 1 = 0

@[simp]

theorem UInt16.mod_one {a : UInt16} : a % 1 = 0

@[simp]

theorem UInt32.mod_one {a : UInt32} : a % 1 = 0

@[simp]

theorem UInt64.mod_one {a : UInt64} : a % 1 = 0

@[simp]

theorem USize.mod_one {a : USize} : a % 1 = 0

@[simp]

theorem UInt8.mod_self {a : UInt8} : a % a = 0

@[simp]

theorem UInt16.mod_self {a : UInt16} : a % a = 0

@[simp]

theorem UInt32.mod_self {a : UInt32} : a % a = 0

@[simp]

theorem UInt64.mod_self {a : UInt64} : a % a = 0

@[simp]

theorem USize.mod_self {a : USize} : a % a = 0

theorem UInt8.pos_iff_ne_zero {a : UInt8} : 0 < a ↔ a ≠ 0

theorem UInt16.pos_iff_ne_zero {a : UInt16} : 0 < a ↔ a ≠ 0

theorem UInt32.pos_iff_ne_zero {a : UInt32} : 0 < a ↔ a ≠ 0

theorem UInt64.pos_iff_ne_zero {a : UInt64} : 0 < a ↔ a ≠ 0

theorem USize.pos_iff_ne_zero {a : USize} : 0 < a ↔ a ≠ 0

theorem UInt8.lt_of_le_of_lt {a b c : UInt8} : a ≤ b → b < c → a < c

theorem UInt16.lt_of_le_of_lt {a b c : UInt16} : a ≤ b → b < c → a < c

theorem UInt32.lt_of_le_of_lt {a b c : UInt32} : a ≤ b → b < c → a < c

theorem UInt64.lt_of_le_of_lt {a b c : UInt64} : a ≤ b → b < c → a < c

theorem USize.lt_of_le_of_lt {a b c : USize} : a ≤ b → b < c → a < c

theorem UInt8.lt_of_lt_of_le {a b c : UInt8} : a < b → b ≤ c → a < c

theorem UInt16.lt_of_lt_of_le {a b c : UInt16} : a < b → b ≤ c → a < c

theorem UInt32.lt_of_lt_of_le {a b c : UInt32} : a < b → b ≤ c → a < c

theorem UInt64.lt_of_lt_of_le {a b c : UInt64} : a < b → b ≤ c → a < c

theorem USize.lt_of_lt_of_le {a b c : USize} : a < b → b ≤ c → a < c

theorem UInt8.lt_or_lt_of_ne {a b : UInt8} : a ≠ b → a < b ∨ b < a

theorem UInt16.lt_or_lt_of_ne {a b : UInt16} : a ≠ b → a < b ∨ b < a

theorem UInt32.lt_or_lt_of_ne {a b : UInt32} : a ≠ b → a < b ∨ b < a

theorem UInt64.lt_or_lt_of_ne {a b : UInt64} : a ≠ b → a < b ∨ b < a

theorem USize.lt_or_lt_of_ne {a b : USize} : a ≠ b → a < b ∨ b < a

theorem UInt8.lt_or_le (a b : UInt8) : a < b ∨ b ≤ a

theorem UInt16.lt_or_le (a b : UInt16) : a < b ∨ b ≤ a

theorem UInt32.lt_or_le (a b : UInt32) : a < b ∨ b ≤ a

theorem UInt64.lt_or_le (a b : UInt64) : a < b ∨ b ≤ a

theorem USize.lt_or_le (a b : USize) : a < b ∨ b ≤ a

theorem UInt8.le_or_lt (a b : UInt8) : a ≤ b ∨ b < a

theorem UInt16.le_or_lt (a b : UInt16) : a ≤ b ∨ b < a

theorem UInt32.le_or_lt (a b : UInt32) : a ≤ b ∨ b < a

theorem UInt64.le_or_lt (a b : UInt64) : a ≤ b ∨ b < a

theorem USize.le_or_lt (a b : USize) : a ≤ b ∨ b < a

theorem UInt8.le_of_eq {a b : UInt8} : a = b → a ≤ b

theorem UInt16.le_of_eq {a b : UInt16} : a = b → a ≤ b

theorem UInt32.le_of_eq {a b : UInt32} : a = b → a ≤ b

theorem UInt64.le_of_eq {a b : UInt64} : a = b → a ≤ b

theorem USize.le_of_eq {a b : USize} : a = b → a ≤ b

theorem UInt8.le_iff_lt_or_eq {a b : UInt8} : a ≤ b ↔ a < b ∨ a = b

theorem UInt16.le_iff_lt_or_eq {a b : UInt16} : a ≤ b ↔ a < b ∨ a = b

theorem UInt32.le_iff_lt_or_eq {a b : UInt32} : a ≤ b ↔ a < b ∨ a = b

theorem UInt64.le_iff_lt_or_eq {a b : UInt64} : a ≤ b ↔ a < b ∨ a = b

theorem USize.le_iff_lt_or_eq {a b : USize} : a ≤ b ↔ a < b ∨ a = b

theorem UInt8.lt_or_eq_of_le {a b : UInt8} : a ≤ b → a < b ∨ a = b

theorem UInt16.lt_or_eq_of_le {a b : UInt16} : a ≤ b → a < b ∨ a = b

theorem UInt32.lt_or_eq_of_le {a b : UInt32} : a ≤ b → a < b ∨ a = b

theorem UInt64.lt_or_eq_of_le {a b : UInt64} : a ≤ b → a < b ∨ a = b

theorem USize.lt_or_eq_of_le {a b : USize} : a ≤ b → a < b ∨ a = b

theorem UInt8.sub_le {a b : UInt8} (hab : b ≤ a) : a - b ≤ a

theorem UInt16.sub_le {a b : UInt16} (hab : b ≤ a) : a - b ≤ a

theorem UInt32.sub_le {a b : UInt32} (hab : b ≤ a) : a - b ≤ a

theorem UInt64.sub_le {a b : UInt64} (hab : b ≤ a) : a - b ≤ a

theorem USize.sub_le {a b : USize} (hab : b ≤ a) : a - b ≤ a

theorem UInt8.sub_lt {a b : UInt8} (hb : 0 < b) (hab : b ≤ a) : a - b < a

theorem UInt16.sub_lt {a b : UInt16} (hb : 0 < b) (hab : b ≤ a) : a - b < a

theorem UInt32.sub_lt {a b : UInt32} (hb : 0 < b) (hab : b ≤ a) : a - b < a

theorem UInt64.sub_lt {a b : UInt64} (hb : 0 < b) (hab : b ≤ a) : a - b < a

theorem USize.sub_lt {a b : USize} (hb : 0 < b) (hab : b ≤ a) : a - b < a

theorem UInt8.lt_add_one {c : UInt8} (h : c ≠ -1) : c < c + 1

theorem UInt16.lt_add_one {c : UInt16} (h : c ≠ -1) : c < c + 1

theorem UInt32.lt_add_one {c : UInt32} (h : c ≠ -1) : c < c + 1

theorem UInt64.lt_add_one {c : UInt64} (h : c ≠ -1) : c < c + 1

theorem USize.lt_add_one {c : USize} (h : c ≠ -1) : c < c + 1

theorem UInt8.toNat_ofNat_le {n : Nat} : (ofNat n).toNat ≤ n

theorem UInt16.toNat_ofNat_le {n : Nat} : (ofNat n).toNat ≤ n

theorem UInt32.toNat_ofNat_le {n : Nat} : (ofNat n).toNat ≤ n

theorem UInt64.toNat_ofNat_le {n : Nat} : (ofNat n).toNat ≤ n

theorem USize.toNat_ofNat_le {n : Nat} : (ofNat n).toNat ≤ n