def commandDeclare_int_theorems__ : Lean.ParserDescr

Equations

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

@[simp]

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

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

theorem Int8.ofBitVec_inj {a b : BitVec 8} : ofBitVec a = ofBitVec b ↔ a = b

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Int8.toBitVec_ofNat' {n : Nat} : (ofNat n).toBitVec = BitVec.ofNat 8 n

theorem Int8.eq_iff_ofBitVec_eq {a b : BitVec 8} : a = b ↔ ofBitVec a = ofBitVec b

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

theorem Int8.lt_iff_toBitVec_slt {a b : Int8} : a < b ↔ a.toBitVec.slt b.toBitVec = true

@[simp]

theorem Int8.toBitVec_ofNat {n : Nat} : (OfNat.ofNat n).toBitVec = OfNat.ofNat n

theorem Int8.le_iff_toBitVec_sle {a b : Int8} : a ≤ b ↔ a.toBitVec.sle b.toBitVec = true

theorem Int8.ne_iff_ofBitVec_ne {a b : BitVec 8} : a ≠ b ↔ ofBitVec a ≠ ofBitVec b

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

@[simp]

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

@[simp]

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

theorem Int16.le_iff_toBitVec_sle {a b : Int16} : a ≤ b ↔ a.toBitVec.sle b.toBitVec = true

@[simp]

theorem Int16.toBitVec_ofNat {n : Nat} : (OfNat.ofNat n).toBitVec = OfNat.ofNat n

theorem Int16.eq_iff_ofBitVec_eq {a b : BitVec 16} : a = b ↔ ofBitVec a = ofBitVec b

theorem Int16.lt_iff_toBitVec_slt {a b : Int16} : a < b ↔ a.toBitVec.slt b.toBitVec = true

@[simp]

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

@[simp]

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

theorem Int16.ofBitVec_inj {a b : BitVec 16} : ofBitVec a = ofBitVec b ↔ a = b

theorem Int16.ne_iff_ofBitVec_ne {a b : BitVec 16} : a ≠ b ↔ ofBitVec a ≠ ofBitVec b

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

@[simp]

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

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

@[simp]

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

@[simp]

theorem Int16.toBitVec_ofNat' {n : Nat} : (ofNat n).toBitVec = BitVec.ofNat 16 n

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

@[simp]

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

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

theorem Int32.eq_iff_ofBitVec_eq {a b : BitVec 32} : a = b ↔ ofBitVec a = ofBitVec b

@[simp]

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

@[simp]

theorem Int32.toBitVec_ofNat' {n : Nat} : (ofNat n).toBitVec = BitVec.ofNat 32 n

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

theorem Int32.le_iff_toBitVec_sle {a b : Int32} : a ≤ b ↔ a.toBitVec.sle b.toBitVec = true

@[simp]

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

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

theorem Int32.ofBitVec_inj {a b : BitVec 32} : ofBitVec a = ofBitVec b ↔ a = b

@[simp]

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

@[simp]

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

@[simp]

theorem Int32.toBitVec_ofNat {n : Nat} : (OfNat.ofNat n).toBitVec = OfNat.ofNat n

theorem Int32.lt_iff_toBitVec_slt {a b : Int32} : a < b ↔ a.toBitVec.slt b.toBitVec = true

theorem Int32.ne_iff_ofBitVec_ne {a b : BitVec 32} : a ≠ b ↔ ofBitVec a ≠ ofBitVec b

@[simp]

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

theorem Int64.eq_iff_ofBitVec_eq {a b : BitVec 64} : a = b ↔ ofBitVec a = ofBitVec b

theorem Int64.ofBitVec_inj {a b : BitVec 64} : ofBitVec a = ofBitVec b ↔ a = b

theorem Int64.le_iff_toBitVec_sle {a b : Int64} : a ≤ b ↔ a.toBitVec.sle b.toBitVec = true

@[simp]

theorem Int64.toBitVec_ofNat' {n : Nat} : (ofNat n).toBitVec = BitVec.ofNat 64 n

@[simp]

theorem Int64.toBitVec_ofNat {n : Nat} : (OfNat.ofNat n).toBitVec = OfNat.ofNat n

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

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

theorem Int64.ne_iff_ofBitVec_ne {a b : BitVec 64} : a ≠ b ↔ ofBitVec a ≠ ofBitVec b

theorem Int64.lt_iff_toBitVec_slt {a b : Int64} : a < b ↔ a.toBitVec.slt b.toBitVec = true

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem ISize.toBitVec_ofNat {n : Nat} : (OfNat.ofNat n).toBitVec = OfNat.ofNat n

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

@[simp]

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

theorem ISize.eq_iff_ofBitVec_eq {a b : BitVec System.Platform.numBits} : a = b ↔ ofBitVec a = ofBitVec b

theorem ISize.ofBitVec_inj {a b : BitVec System.Platform.numBits} : ofBitVec a = ofBitVec b ↔ a = b

@[simp]

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

@[simp]

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

theorem ISize.ne_iff_ofBitVec_ne {a b : BitVec System.Platform.numBits} : a ≠ b ↔ ofBitVec a ≠ ofBitVec b

theorem ISize.lt_iff_toBitVec_slt {a b : ISize} : a < b ↔ a.toBitVec.slt b.toBitVec = true

theorem ISize.le_iff_toBitVec_sle {a b : ISize} : a ≤ b ↔ a.toBitVec.sle b.toBitVec = true

@[simp]

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

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

theorem Int8.toInt.inj {x y : Int8} (h : x.toInt = y.toInt) : x = y

theorem Int8.toInt_inj {x y : Int8} : x.toInt = y.toInt ↔ x = y

theorem Int16.toInt.inj {x y : Int16} (h : x.toInt = y.toInt) : x = y

theorem Int16.toInt_inj {x y : Int16} : x.toInt = y.toInt ↔ x = y

theorem Int32.toInt.inj {x y : Int32} (h : x.toInt = y.toInt) : x = y

theorem Int32.toInt_inj {x y : Int32} : x.toInt = y.toInt ↔ x = y

theorem Int64.toInt.inj {x y : Int64} (h : x.toInt = y.toInt) : x = y

theorem Int64.toInt_inj {x y : Int64} : x.toInt = y.toInt ↔ x = y

theorem ISize.toInt.inj {x y : ISize} (h : x.toInt = y.toInt) : x = y

theorem ISize.toInt_inj {x y : ISize} : x.toInt = y.toInt ↔ x = y

@[simp]

theorem Int8.toBitVec_neg (x : Int8) : (-x).toBitVec = -x.toBitVec

@[simp]

theorem Int16.toBitVec_neg (x : Int16) : (-x).toBitVec = -x.toBitVec

@[simp]

theorem Int32.toBitVec_neg (x : Int32) : (-x).toBitVec = -x.toBitVec

@[simp]

theorem Int64.toBitVec_neg (x : Int64) : (-x).toBitVec = -x.toBitVec

@[simp]

theorem ISize.toBitVec_neg (x : ISize) : (-x).toBitVec = -x.toBitVec

@[simp]

theorem Int8.toBitVec_zero : toBitVec 0 = 0#8

@[simp]

theorem Int16.toBitVec_zero : toBitVec 0 = 0#16

@[simp]

theorem Int32.toBitVec_zero : toBitVec 0 = 0#32

@[simp]

theorem Int64.toBitVec_zero : toBitVec 0 = 0#64

@[simp]

theorem ISize.toBitVec_zero : toBitVec 0 = 0#System.Platform.numBits

theorem Int8.toBitVec_one : toBitVec 1 = 1#8

theorem Int16.toBitVec_one : toBitVec 1 = 1#16

theorem Int32.toBitVec_one : toBitVec 1 = 1#32

theorem Int64.toBitVec_one : toBitVec 1 = 1#64

theorem ISize.toBitVec_one : toBitVec 1 = 1#System.Platform.numBits

@[simp]

theorem Int8.toBitVec_ofInt (i : Int) : (ofInt i).toBitVec = BitVec.ofInt 8 i

@[simp]

theorem Int16.toBitVec_ofInt (i : Int) : (ofInt i).toBitVec = BitVec.ofInt 16 i

@[simp]

theorem Int32.toBitVec_ofInt (i : Int) : (ofInt i).toBitVec = BitVec.ofInt 32 i

@[simp]

theorem Int64.toBitVec_ofInt (i : Int) : (ofInt i).toBitVec = BitVec.ofInt 64 i

@[simp]

theorem ISize.toBitVec_ofInt (i : Int) : (ofInt i).toBitVec = BitVec.ofInt System.Platform.numBits i

@[simp]

theorem Int8.neg_zero : -0 = 0

@[simp]

theorem Int16.neg_zero : -0 = 0

@[simp]

theorem Int32.neg_zero : -0 = 0

@[simp]

theorem Int64.neg_zero : -0 = 0

@[simp]

theorem ISize.neg_zero : -0 = 0

theorem ISize.toNat_toBitVec_ofNat_of_lt {n : Nat} (h : n < 2 ^ 32) : (ofNat n).toBitVec.toNat = n

@[simp]

theorem Int8.toInt_ofInt {n : Int} : (ofInt n).toInt = n.bmod size

@[simp]

theorem Int16.toInt_ofInt {n : Int} : (ofInt n).toInt = n.bmod size

@[simp]

theorem Int32.toInt_ofInt {n : Int} : (ofInt n).toInt = n.bmod size

@[simp]

theorem Int64.toInt_ofInt {n : Int} : (ofInt n).toInt = n.bmod size

theorem ISize.toInt_ofInt {n : Int} : (ofInt n).toInt = n.bmod size

@[simp]

theorem Int8.toInt_ofNat' {n : Nat} : (ofNat n).toInt = (↑n).bmod size

@[simp]

theorem Int16.toInt_ofNat' {n : Nat} : (ofNat n).toInt = (↑n).bmod size

@[simp]

theorem Int32.toInt_ofNat' {n : Nat} : (ofNat n).toInt = (↑n).bmod size

@[simp]

theorem Int64.toInt_ofNat' {n : Nat} : (ofNat n).toInt = (↑n).bmod size

@[simp]

theorem ISize.toInt_ofNat' {n : Nat} : (ofNat n).toInt = (↑n).bmod size

theorem Int8.toInt_ofNat {n : Nat} : (OfNat.ofNat n).toInt = (↑n).bmod size

theorem Int16.toInt_ofNat {n : Nat} : (OfNat.ofNat n).toInt = (↑n).bmod size

theorem Int32.toInt_ofNat {n : Nat} : (OfNat.ofNat n).toInt = (↑n).bmod size

theorem Int64.toInt_ofNat {n : Nat} : (OfNat.ofNat n).toInt = (↑n).bmod size

theorem ISize.toInt_ofNat {n : Nat} : (OfNat.ofNat n).toInt = (↑n).bmod size

theorem Int8.toInt_ofInt_of_le {n : Int} (hn : -2 ^ 7 ≤ n) (hn' : n < 2 ^ 7) : (ofInt n).toInt = n

theorem Int16.toInt_ofInt_of_le {n : Int} (hn : -2 ^ 15 ≤ n) (hn' : n < 2 ^ 15) : (ofInt n).toInt = n

theorem Int32.toInt_ofInt_of_le {n : Int} (hn : -2 ^ 31 ≤ n) (hn' : n < 2 ^ 31) : (ofInt n).toInt = n

theorem Int64.toInt_ofInt_of_le {n : Int} (hn : -2 ^ 63 ≤ n) (hn' : n < 2 ^ 63) : (ofInt n).toInt = n

theorem ISize.toInt_ofInt_of_le {n : Int} (hn : -2 ^ 31 ≤ n) (hn' : n < 2 ^ 31) : (ofInt n).toInt = n

theorem ISize.toInt_ofInt_of_two_pow_numBits_le {n : Int} (hn : -2 ^ (System.Platform.numBits - 1) ≤ n) (hn' : n < 2 ^ (System.Platform.numBits - 1)) : (ofInt n).toInt = n

theorem ISize.toNatClampNeg_ofInt_eq_zero {n : Int} (hn : -2 ^ 31 ≤ n) (hn' : n ≤ 0) : (ofInt n).toNatClampNeg = 0

theorem Int8.neg_ofInt {n : Int} : -ofInt n = ofInt (-n)

theorem Int16.neg_ofInt {n : Int} : -ofInt n = ofInt (-n)

theorem Int32.neg_ofInt {n : Int} : -ofInt n = ofInt (-n)

theorem Int64.neg_ofInt {n : Int} : -ofInt n = ofInt (-n)

theorem ISize.neg_ofInt {n : Int} : -ofInt n = ofInt (-n)

theorem Int8.ofInt_eq_ofNat {n : Nat} : ofInt ↑n = ofNat n

theorem Int16.ofInt_eq_ofNat {n : Nat} : ofInt ↑n = ofNat n

theorem Int32.ofInt_eq_ofNat {n : Nat} : ofInt ↑n = ofNat n

theorem Int64.ofInt_eq_ofNat {n : Nat} : ofInt ↑n = ofNat n

theorem ISize.ofInt_eq_ofNat {n : Nat} : ofInt ↑n = ofNat n

theorem Int8.neg_ofNat {n : Nat} : -ofNat n = ofInt (-↑n)

theorem Int16.neg_ofNat {n : Nat} : -ofNat n = ofInt (-↑n)

theorem Int32.neg_ofNat {n : Nat} : -ofNat n = ofInt (-↑n)

theorem Int64.neg_ofNat {n : Nat} : -ofNat n = ofInt (-↑n)

theorem ISize.neg_ofNat {n : Nat} : -ofNat n = ofInt (-↑n)

theorem Int8.toNatClampNeg_ofNat_of_lt {n : Nat} (h : n < 2 ^ 7) : (ofNat n).toNatClampNeg = n

theorem Int16.toNatClampNeg_ofNat_of_lt {n : Nat} (h : n < 2 ^ 15) : (ofNat n).toNatClampNeg = n

theorem Int32.toNatClampNeg_ofNat_of_lt {n : Nat} (h : n < 2 ^ 31) : (ofNat n).toNatClampNeg = n

theorem Int64.toNatClampNeg_ofNat_of_lt {n : Nat} (h : n < 2 ^ 63) : (ofNat n).toNatClampNeg = n

theorem ISize.toNatClampNeg_ofNat_of_lt {n : Nat} (h : n < 2 ^ 31) : (ofNat n).toNatClampNeg = n

theorem ISize.toNatClampNeg_ofNat_of_lt_two_pow_numBits {n : Nat} (h : n < 2 ^ (System.Platform.numBits - 1)) : (ofNat n).toNatClampNeg = n

theorem ISize.toNatClampNeg_neg_ofNat_of_le {n : Nat} (h : n ≤ 2 ^ 31) : (-ofNat n).toNatClampNeg = 0

theorem Int8.toInt_ofNat_of_lt {n : Nat} (h : n < 2 ^ 7) : (ofNat n).toInt = ↑n

theorem Int16.toInt_ofNat_of_lt {n : Nat} (h : n < 2 ^ 15) : (ofNat n).toInt = ↑n

theorem Int32.toInt_ofNat_of_lt {n : Nat} (h : n < 2 ^ 31) : (ofNat n).toInt = ↑n

theorem Int64.toInt_ofNat_of_lt {n : Nat} (h : n < 2 ^ 63) : (ofNat n).toInt = ↑n

theorem ISize.toInt_ofNat_of_lt {n : Nat} (h : n < 2 ^ 31) : (ofNat n).toInt = ↑n

theorem ISize.toInt_ofNat_of_lt_two_pow_numBits {n : Nat} (h : n < 2 ^ (System.Platform.numBits - 1)) : (ofNat n).toInt = ↑n

theorem Int64.toInt_neg_ofNat_of_le {n : Nat} (h : n ≤ 2 ^ 63) : (-ofNat n).toInt = -↑n

theorem ISize.toInt_neg_ofNat_of_le {n : Nat} (h : n ≤ 2 ^ 31) : (-ofNat n).toInt = -↑n

theorem Int8.toInt_zero : toInt 0 = 0

theorem Int16.toInt_zero : toInt 0 = 0

theorem Int32.toInt_zero : toInt 0 = 0

theorem Int64.toInt_zero : toInt 0 = 0

theorem ISize.toInt_zero : toInt 0 = 0

theorem Int8.toInt_minValue : minValue.toInt = -2 ^ 7

theorem Int16.toInt_minValue : minValue.toInt = -2 ^ 15

theorem Int32.toInt_minValue : minValue.toInt = -2 ^ 31

theorem Int64.toInt_minValue : minValue.toInt = -2 ^ 63

theorem ISize.toInt_minValue : minValue.toInt = -2 ^ (System.Platform.numBits - 1)

theorem Int8.toInt_maxValue : maxValue.toInt = 2 ^ 7 - 1

theorem Int16.toInt_maxValue : maxValue.toInt = 2 ^ 15 - 1

theorem Int32.toInt_maxValue : maxValue.toInt = 2 ^ 31 - 1

theorem Int64.toInt_maxValue : maxValue.toInt = 2 ^ 63 - 1

theorem ISize.toInt_maxValue : maxValue.toInt = 2 ^ (System.Platform.numBits - 1) - 1

@[simp]

theorem Int8.toNatClampNeg_minValue : minValue.toNatClampNeg = 0

@[simp]

theorem Int16.toNatClampNeg_minValue : minValue.toNatClampNeg = 0

@[simp]

theorem Int32.toNatClampNeg_minValue : minValue.toNatClampNeg = 0

@[simp]

theorem Int64.toNatClampNeg_minValue : minValue.toNatClampNeg = 0

@[simp]

theorem ISize.toNatClampNeg_minValue : minValue.toNatClampNeg = 0

@[simp]

theorem UInt8.toBitVec_toInt8 (x : UInt8) : x.toInt8.toBitVec = x.toBitVec

@[simp]

theorem UInt16.toBitVec_toInt16 (x : UInt16) : x.toInt16.toBitVec = x.toBitVec

@[simp]

theorem UInt32.toBitVec_toInt32 (x : UInt32) : x.toInt32.toBitVec = x.toBitVec

@[simp]

theorem UInt64.toBitVec_toInt64 (x : UInt64) : x.toInt64.toBitVec = x.toBitVec

@[simp]

theorem USize.toBitVec_toISize (x : USize) : x.toISize.toBitVec = x.toBitVec

@[simp]

theorem Int8.ofBitVec_uInt8ToBitVec (x : UInt8) : ofBitVec x.toBitVec = x.toInt8

@[simp]

theorem Int16.ofBitVec_uInt16ToBitVec (x : UInt16) : ofBitVec x.toBitVec = x.toInt16

@[simp]

theorem Int32.ofBitVec_uInt32ToBitVec (x : UInt32) : ofBitVec x.toBitVec = x.toInt32

@[simp]

theorem Int64.ofBitVec_uInt64ToBitVec (x : UInt64) : ofBitVec x.toBitVec = x.toInt64

@[simp]

theorem ISize.ofBitVec_uSizeToBitVec (x : USize) : ofBitVec x.toBitVec = x.toISize

@[simp]

theorem UInt8.toUInt8_toInt8 (x : UInt8) : x.toInt8.toUInt8 = x

@[simp]

theorem UInt16.toUInt16_toInt16 (x : UInt16) : x.toInt16.toUInt16 = x

@[simp]

theorem UInt32.toUInt32_toInt32 (x : UInt32) : x.toInt32.toUInt32 = x

@[simp]

theorem UInt64.toUInt64_toInt64 (x : UInt64) : x.toInt64.toUInt64 = x

@[simp]

theorem USize.toUSize_toISize (x : USize) : x.toISize.toUSize = x

@[simp]

theorem Int8.toNat_toInt (x : Int8) : x.toInt.toNat = x.toNatClampNeg

@[simp]

theorem Int16.toNat_toInt (x : Int16) : x.toInt.toNat = x.toNatClampNeg

@[simp]

theorem Int32.toNat_toInt (x : Int32) : x.toInt.toNat = x.toNatClampNeg

@[simp]

theorem Int64.toNat_toInt (x : Int64) : x.toInt.toNat = x.toNatClampNeg

@[simp]

theorem ISize.toNat_toInt (x : ISize) : x.toInt.toNat = x.toNatClampNeg

@[simp]

theorem Int8.toInt_toBitVec (x : Int8) : x.toBitVec.toInt = x.toInt

@[simp]

theorem Int16.toInt_toBitVec (x : Int16) : x.toBitVec.toInt = x.toInt

@[simp]

theorem Int32.toInt_toBitVec (x : Int32) : x.toBitVec.toInt = x.toInt

@[simp]

theorem Int64.toInt_toBitVec (x : Int64) : x.toBitVec.toInt = x.toInt

@[simp]

theorem ISize.toInt_toBitVec (x : ISize) : x.toBitVec.toInt = x.toInt

@[simp]

theorem Int8.toBitVec_toInt16 (x : Int8) : x.toInt16.toBitVec = BitVec.signExtend 16 x.toBitVec

@[simp]

theorem Int8.toBitVec_toInt32 (x : Int8) : x.toInt32.toBitVec = BitVec.signExtend 32 x.toBitVec

@[simp]

theorem Int8.toBitVec_toInt64 (x : Int8) : x.toInt64.toBitVec = BitVec.signExtend 64 x.toBitVec

@[simp]

theorem Int8.toBitVec_toISize (x : Int8) : x.toISize.toBitVec = BitVec.signExtend System.Platform.numBits x.toBitVec

@[simp]

theorem Int16.toBitVec_toInt8 (x : Int16) : x.toInt8.toBitVec = BitVec.signExtend 8 x.toBitVec

@[simp]

theorem Int16.toBitVec_toInt32 (x : Int16) : x.toInt32.toBitVec = BitVec.signExtend 32 x.toBitVec

@[simp]

theorem Int16.toBitVec_toInt64 (x : Int16) : x.toInt64.toBitVec = BitVec.signExtend 64 x.toBitVec

@[simp]

theorem Int16.toBitVec_toISize (x : Int16) : x.toISize.toBitVec = BitVec.signExtend System.Platform.numBits x.toBitVec

@[simp]

theorem Int32.toBitVec_toInt8 (x : Int32) : x.toInt8.toBitVec = BitVec.signExtend 8 x.toBitVec

@[simp]

theorem Int32.toBitVec_toInt16 (x : Int32) : x.toInt16.toBitVec = BitVec.signExtend 16 x.toBitVec

@[simp]

theorem Int32.toBitVec_toInt64 (x : Int32) : x.toInt64.toBitVec = BitVec.signExtend 64 x.toBitVec

@[simp]

theorem Int32.toBitVec_toISize (x : Int32) : x.toISize.toBitVec = BitVec.signExtend System.Platform.numBits x.toBitVec

@[simp]

theorem Int64.toBitVec_toInt8 (x : Int64) : x.toInt8.toBitVec = BitVec.signExtend 8 x.toBitVec

@[simp]

theorem Int64.toBitVec_toInt16 (x : Int64) : x.toInt16.toBitVec = BitVec.signExtend 16 x.toBitVec

@[simp]

theorem Int64.toBitVec_toInt32 (x : Int64) : x.toInt32.toBitVec = BitVec.signExtend 32 x.toBitVec

@[simp]

theorem Int64.toBitVec_toISize (x : Int64) : x.toISize.toBitVec = BitVec.signExtend System.Platform.numBits x.toBitVec

@[simp]

theorem ISize.toBitVec_toInt8 (x : ISize) : x.toInt8.toBitVec = BitVec.signExtend 8 x.toBitVec

@[simp]

theorem ISize.toBitVec_toInt16 (x : ISize) : x.toInt16.toBitVec = BitVec.signExtend 16 x.toBitVec

@[simp]

theorem ISize.toBitVec_toInt32 (x : ISize) : x.toInt32.toBitVec = BitVec.signExtend 32 x.toBitVec

@[simp]

theorem ISize.toBitVec_toInt64 (x : ISize) : x.toInt64.toBitVec = BitVec.signExtend 64 x.toBitVec

theorem Int8.toInt_lt (x : Int8) : x.toInt < 2 ^ 7

theorem Int8.le_toInt (x : Int8) : -2 ^ 7 ≤ x.toInt

theorem Int16.toInt_lt (x : Int16) : x.toInt < 2 ^ 15

theorem Int16.le_toInt (x : Int16) : -2 ^ 15 ≤ x.toInt

theorem Int32.toInt_lt (x : Int32) : x.toInt < 2 ^ 31

theorem Int32.le_toInt (x : Int32) : -2 ^ 31 ≤ x.toInt

theorem Int64.toInt_lt (x : Int64) : x.toInt < 2 ^ 63

theorem Int64.le_toInt (x : Int64) : -2 ^ 63 ≤ x.toInt

theorem ISize.toInt_lt_two_pow_numBits (x : ISize) : x.toInt < 2 ^ (System.Platform.numBits - 1)

theorem ISize.two_pow_numBits_le_toInt (x : ISize) : -2 ^ (System.Platform.numBits - 1) ≤ x.toInt

theorem ISize.toInt_lt (x : ISize) : x.toInt < 2 ^ 63

theorem ISize.le_toInt (x : ISize) : -2 ^ 63 ≤ x.toInt

theorem Int8.toInt_le (x : Int8) : x.toInt ≤ maxValue.toInt

theorem Int16.toInt_le (x : Int16) : x.toInt ≤ maxValue.toInt

theorem Int32.toInt_le (x : Int32) : x.toInt ≤ maxValue.toInt

theorem Int64.toInt_le (x : Int64) : x.toInt ≤ maxValue.toInt

theorem ISize.toInt_le (x : ISize) : x.toInt ≤ maxValue.toInt

theorem Int8.minValue_le_toInt (x : Int8) : minValue.toInt ≤ x.toInt

theorem Int16.minValue_le_toInt (x : Int16) : minValue.toInt ≤ x.toInt

theorem Int32.minValue_le_toInt (x : Int32) : minValue.toInt ≤ x.toInt

theorem Int64.minValue_le_toInt (x : Int64) : minValue.toInt ≤ x.toInt

theorem ISize.minValue_le_toInt (x : ISize) : minValue.toInt ≤ x.toInt

theorem ISize.toInt_minValue_le : minValue.toInt ≤ -2 ^ 31

theorem ISize.le_toInt_maxValue : 2 ^ 31 - 1 ≤ maxValue.toInt

theorem Int8.iSizeMinValue_le_toInt (x : Int8) : ISize.minValue.toInt ≤ x.toInt

theorem Int8.toInt_le_iSizeMaxValue (x : Int8) : x.toInt ≤ ISize.maxValue.toInt

theorem Int16.iSizeMinValue_le_toInt (x : Int16) : ISize.minValue.toInt ≤ x.toInt

theorem Int16.toInt_le_iSizeMaxValue (x : Int16) : x.toInt ≤ ISize.maxValue.toInt

theorem Int32.iSizeMinValue_le_toInt (x : Int32) : ISize.minValue.toInt ≤ x.toInt

theorem Int32.toInt_le_iSizeMaxValue (x : Int32) : x.toInt ≤ ISize.maxValue.toInt

theorem ISize.int64MinValue_le_toInt (x : ISize) : Int64.minValue.toInt ≤ x.toInt

theorem ISize.toInt_le_int64MaxValue (x : ISize) : x.toInt ≤ Int64.maxValue.toInt

theorem Int8.toNatClampNeg_lt (x : Int8) : x.toNatClampNeg < 2 ^ 7

theorem Int16.toNatClampNeg_lt (x : Int16) : x.toNatClampNeg < 2 ^ 15

theorem Int32.toNatClampNeg_lt (x : Int32) : x.toNatClampNeg < 2 ^ 31

theorem Int64.toNatClampNeg_lt (x : Int64) : x.toNatClampNeg < 2 ^ 63

theorem ISize.toNatClampNeg_lt_two_pow_numBits (x : ISize) : x.toNatClampNeg < 2 ^ (System.Platform.numBits - 1)

theorem ISize.toNatClampNeg_lt (x : ISize) : x.toNatClampNeg < 2 ^ 63

@[simp]

theorem Int8.toInt_toInt16 (x : Int8) : x.toInt16.toInt = x.toInt

@[simp]

theorem Int8.toInt_toInt32 (x : Int8) : x.toInt32.toInt = x.toInt

@[simp]

theorem Int8.toInt_toInt64 (x : Int8) : x.toInt64.toInt = x.toInt

@[simp]

theorem Int8.toInt_toISize (x : Int8) : x.toISize.toInt = x.toInt

@[simp]

theorem Int16.toInt_toInt8 (x : Int16) : x.toInt8.toInt = x.toInt.bmod (2 ^ 8)

@[simp]

theorem Int16.toInt_toInt32 (x : Int16) : x.toInt32.toInt = x.toInt

@[simp]

theorem Int16.toInt_toInt64 (x : Int16) : x.toInt64.toInt = x.toInt

@[simp]

theorem Int16.toInt_toISize (x : Int16) : x.toISize.toInt = x.toInt

@[simp]

theorem Int32.toInt_toInt8 (x : Int32) : x.toInt8.toInt = x.toInt.bmod (2 ^ 8)

@[simp]

theorem Int32.toInt_toInt16 (x : Int32) : x.toInt16.toInt = x.toInt.bmod (2 ^ 16)

@[simp]

theorem Int32.toInt_toInt64 (x : Int32) : x.toInt64.toInt = x.toInt

@[simp]

theorem Int32.toInt_toISize (x : Int32) : x.toISize.toInt = x.toInt

@[simp]

theorem Int64.toInt_toInt8 (x : Int64) : x.toInt8.toInt = x.toInt.bmod (2 ^ 8)

@[simp]

theorem Int64.toInt_toInt16 (x : Int64) : x.toInt16.toInt = x.toInt.bmod (2 ^ 16)

@[simp]

theorem Int64.toInt_toInt32 (x : Int64) : x.toInt32.toInt = x.toInt.bmod (2 ^ 32)

@[simp]

theorem Int64.toInt_toISize (x : Int64) : x.toISize.toInt = x.toInt.bmod (2 ^ System.Platform.numBits)

@[simp]

theorem ISize.toInt_toInt8 (x : ISize) : x.toInt8.toInt = x.toInt.bmod (2 ^ 8)

@[simp]

theorem ISize.toInt_toInt16 (x : ISize) : x.toInt16.toInt = x.toInt.bmod (2 ^ 16)

@[simp]

theorem ISize.toInt_toInt32 (x : ISize) : x.toInt32.toInt = x.toInt.bmod (2 ^ 32)

@[simp]

theorem ISize.toInt_toInt64 (x : ISize) : x.toInt64.toInt = x.toInt

@[simp]

theorem Int8.toNatClampNeg_toInt16 (x : Int8) : x.toInt16.toNatClampNeg = x.toNatClampNeg

@[simp]

theorem Int8.toNatClampNeg_toInt32 (x : Int8) : x.toInt32.toNatClampNeg = x.toNatClampNeg

@[simp]

theorem Int8.toNatClampNeg_toInt64 (x : Int8) : x.toInt64.toNatClampNeg = x.toNatClampNeg

@[simp]

theorem Int8.toNatClampNeg_toISize (x : Int8) : x.toISize.toNatClampNeg = x.toNatClampNeg

@[simp]

theorem Int16.toNatClampNeg_toInt32 (x : Int16) : x.toInt32.toNatClampNeg = x.toNatClampNeg

@[simp]

theorem Int16.toNatClampNeg_toInt64 (x : Int16) : x.toInt64.toNatClampNeg = x.toNatClampNeg

@[simp]

theorem Int16.toNatClampNeg_toISize (x : Int16) : x.toISize.toNatClampNeg = x.toNatClampNeg

@[simp]

theorem Int32.toNatClampNeg_toInt64 (x : Int32) : x.toInt64.toNatClampNeg = x.toNatClampNeg

@[simp]

theorem Int32.toNatClampNeg_toISize (x : Int32) : x.toISize.toNatClampNeg = x.toNatClampNeg

@[simp]

theorem ISize.toNatClampNeg_toInt64 (x : ISize) : x.toInt64.toNatClampNeg = x.toNatClampNeg

@[simp]

theorem Int8.toInt8_toUInt8 (x : Int8) : x.toUInt8.toInt8 = x

@[simp]

theorem Int16.toInt16_toUInt16 (x : Int16) : x.toUInt16.toInt16 = x

@[simp]

theorem Int32.toInt32_toUInt32 (x : Int32) : x.toUInt32.toInt32 = x

@[simp]

theorem Int64.toInt64_toUInt64 (x : Int64) : x.toUInt64.toInt64 = x

@[simp]

theorem ISize.toISize_toUSize (x : ISize) : x.toUSize.toISize = x

theorem Int8.toNat_toBitVec (x : Int8) : x.toBitVec.toNat = x.toUInt8.toNat

theorem Int16.toNat_toBitVec (x : Int16) : x.toBitVec.toNat = x.toUInt16.toNat

theorem Int32.toNat_toBitVec (x : Int32) : x.toBitVec.toNat = x.toUInt32.toNat

theorem Int64.toNat_toBitVec (x : Int64) : x.toBitVec.toNat = x.toUInt64.toNat

theorem ISize.toNat_toBitVec (x : ISize) : x.toBitVec.toNat = x.toUSize.toNat

theorem Int8.toNat_toBitVec_of_le {x : Int8} (hx : 0 ≤ x) : x.toBitVec.toNat = x.toNatClampNeg

theorem Int16.toNat_toBitVec_of_le {x : Int16} (hx : 0 ≤ x) : x.toBitVec.toNat = x.toNatClampNeg

theorem Int32.toNat_toBitVec_of_le {x : Int32} (hx : 0 ≤ x) : x.toBitVec.toNat = x.toNatClampNeg

theorem Int64.toNat_toBitVec_of_le {x : Int64} (hx : 0 ≤ x) : x.toBitVec.toNat = x.toNatClampNeg

theorem ISize.toNat_toBitVec_of_le {x : ISize} (hx : 0 ≤ x) : x.toBitVec.toNat = x.toNatClampNeg

theorem Int8.toNat_toUInt8_of_le {x : Int8} (hx : 0 ≤ x) : x.toUInt8.toNat = x.toNatClampNeg

theorem Int16.toNat_toUInt16_of_le {x : Int16} (hx : 0 ≤ x) : x.toUInt16.toNat = x.toNatClampNeg

theorem Int32.toNat_toUInt32_of_le {x : Int32} (hx : 0 ≤ x) : x.toUInt32.toNat = x.toNatClampNeg

theorem Int64.toNat_toUInt64_of_le {x : Int64} (hx : 0 ≤ x) : x.toUInt64.toNat = x.toNatClampNeg

theorem ISize.toNat_toUSize_of_le {x : ISize} (hx : 0 ≤ x) : x.toUSize.toNat = x.toNatClampNeg

theorem Int8.toFin_toBitVec (x : Int8) : x.toBitVec.toFin = x.toUInt8.toFin

theorem Int16.toFin_toBitVec (x : Int16) : x.toBitVec.toFin = x.toUInt16.toFin

theorem Int32.toFin_toBitVec (x : Int32) : x.toBitVec.toFin = x.toUInt32.toFin

theorem Int64.toFin_toBitVec (x : Int64) : x.toBitVec.toFin = x.toUInt64.toFin

theorem ISize.toFin_toBitVec (x : ISize) : x.toBitVec.toFin = x.toUSize.toFin

@[simp]

theorem Int8.toBitVec_toUInt8 (x : Int8) : x.toUInt8.toBitVec = x.toBitVec

@[simp]

theorem Int16.toBitVec_toUInt16 (x : Int16) : x.toUInt16.toBitVec = x.toBitVec

@[simp]

theorem Int32.toBitVec_toUInt32 (x : Int32) : x.toUInt32.toBitVec = x.toBitVec

@[simp]

theorem Int64.toBitVec_toUInt64 (x : Int64) : x.toUInt64.toBitVec = x.toBitVec

@[simp]

theorem ISize.toBitVec_toUSize (x : ISize) : x.toUSize.toBitVec = x.toBitVec

@[simp]

theorem UInt8.ofBitVec_int8ToBitVec (x : Int8) : { toBitVec := x.toBitVec } = x.toUInt8

@[simp]

theorem UInt16.ofBitVec_int16ToBitVec (x : Int16) : { toBitVec := x.toBitVec } = x.toUInt16

@[simp]

theorem UInt32.ofBitVec_int32ToBitVec (x : Int32) : { toBitVec := x.toBitVec } = x.toUInt32

@[simp]

theorem UInt64.ofBitVec_int64ToBitVec (x : Int64) : { toBitVec := x.toBitVec } = x.toUInt64

@[simp]

theorem USize.ofBitVec_iSizeToBitVec (x : ISize) : { toBitVec := x.toBitVec } = x.toUSize

@[simp]

theorem Int8.ofBitVec_toBitVec (x : Int8) : ofBitVec x.toBitVec = x

@[simp]

theorem Int16.ofBitVec_toBitVec (x : Int16) : ofBitVec x.toBitVec = x

@[simp]

theorem Int32.ofBitVec_toBitVec (x : Int32) : ofBitVec x.toBitVec = x

@[simp]

theorem Int64.ofBitVec_toBitVec (x : Int64) : ofBitVec x.toBitVec = x

@[simp]

theorem ISize.ofBitVec_toBitVec (x : ISize) : ofBitVec x.toBitVec = x

@[simp]

theorem Int8.ofBitVec_int16ToBitVec (x : Int16) : ofBitVec (BitVec.signExtend 8 x.toBitVec) = x.toInt8

@[simp]

theorem Int8.ofBitVec_int32ToBitVec (x : Int32) : ofBitVec (BitVec.signExtend 8 x.toBitVec) = x.toInt8

@[simp]

theorem Int8.ofBitVec_int64ToBitVec (x : Int64) : ofBitVec (BitVec.signExtend 8 x.toBitVec) = x.toInt8

@[simp]

theorem Int8.ofBitVec_iSizeToBitVec (x : ISize) : ofBitVec (BitVec.signExtend 8 x.toBitVec) = x.toInt8

@[simp]

theorem Int16.ofBitVec_int8ToBitVec (x : Int8) : ofBitVec (BitVec.signExtend 16 x.toBitVec) = x.toInt16

@[simp]

theorem Int16.ofBitVec_int32ToBitVec (x : Int32) : ofBitVec (BitVec.signExtend 16 x.toBitVec) = x.toInt16

@[simp]

theorem Int16.ofBitVec_int64ToBitVec (x : Int64) : ofBitVec (BitVec.signExtend 16 x.toBitVec) = x.toInt16

@[simp]

theorem Int16.ofBitVec_iSizeToBitVec (x : ISize) : ofBitVec (BitVec.signExtend 16 x.toBitVec) = x.toInt16

@[simp]

theorem Int32.ofBitVec_int8ToBitVec (x : Int8) : ofBitVec (BitVec.signExtend 32 x.toBitVec) = x.toInt32

@[simp]

theorem Int32.ofBitVec_int16ToBitVec (x : Int16) : ofBitVec (BitVec.signExtend 32 x.toBitVec) = x.toInt32

@[simp]

theorem Int32.ofBitVec_int64ToBitVec (x : Int64) : ofBitVec (BitVec.signExtend 32 x.toBitVec) = x.toInt32

@[simp]

theorem Int32.ofBitVec_iSizeToBitVec (x : ISize) : ofBitVec (BitVec.signExtend 32 x.toBitVec) = x.toInt32

@[simp]

theorem Int64.ofBitVec_int8ToBitVec (x : Int8) : ofBitVec (BitVec.signExtend 64 x.toBitVec) = x.toInt64

@[simp]

theorem Int64.ofBitVec_int16ToBitVec (x : Int16) : ofBitVec (BitVec.signExtend 64 x.toBitVec) = x.toInt64

@[simp]

theorem Int64.ofBitVec_int32ToBitVec (x : Int32) : ofBitVec (BitVec.signExtend 64 x.toBitVec) = x.toInt64

@[simp]

theorem Int64.ofBitVec_iSizeToBitVec (x : ISize) : ofBitVec (BitVec.signExtend 64 x.toBitVec) = x.toInt64

@[simp]

theorem ISize.ofBitVec_int8ToBitVec (x : Int8) : ofBitVec (BitVec.signExtend System.Platform.numBits x.toBitVec) = x.toISize

@[simp]

theorem ISize.ofBitVec_int16ToBitVec (x : Int16) : ofBitVec (BitVec.signExtend System.Platform.numBits x.toBitVec) = x.toISize

@[simp]

theorem ISize.ofBitVec_int32ToBitVec (x : Int32) : ofBitVec (BitVec.signExtend System.Platform.numBits x.toBitVec) = x.toISize

@[simp]

theorem ISize.ofBitVec_int64ToBitVec (x : Int64) : ofBitVec (BitVec.signExtend System.Platform.numBits x.toBitVec) = x.toISize

@[simp]

theorem Int8.toBitVec_ofIntLE (x : Int) (h₁ : minValue.toInt ≤ x) (h₂ : x ≤ maxValue.toInt) : (ofIntLE x h₁ h₂).toBitVec = BitVec.ofInt 8 x

@[simp]

theorem Int16.toBitVec_ofIntLE (x : Int) (h₁ : minValue.toInt ≤ x) (h₂ : x ≤ maxValue.toInt) : (ofIntLE x h₁ h₂).toBitVec = BitVec.ofInt 16 x

@[simp]

theorem Int32.toBitVec_ofIntLE (x : Int) (h₁ : minValue.toInt ≤ x) (h₂ : x ≤ maxValue.toInt) : (ofIntLE x h₁ h₂).toBitVec = BitVec.ofInt 32 x

@[simp]

theorem Int64.toBitVec_ofIntLE (x : Int) (h₁ : minValue.toInt ≤ x) (h₂ : x ≤ maxValue.toInt) : (ofIntLE x h₁ h₂).toBitVec = BitVec.ofInt 64 x

@[simp]

theorem ISize.toBitVec_ofIntLE (x : Int) (h₁ : minValue.toInt ≤ x) (h₂ : x ≤ maxValue.toInt) : (ofIntLE x h₁ h₂).toBitVec = BitVec.ofInt System.Platform.numBits x

@[simp]

theorem Int8.toInt_bmod (x : Int8) : x.toInt.bmod 256 = x.toInt

@[simp]

theorem Int16.toInt_bmod (x : Int16) : x.toInt.bmod 65536 = x.toInt

@[simp]

theorem Int32.toInt_bmod (x : Int32) : x.toInt.bmod 4294967296 = x.toInt

@[simp]

theorem Int64.toInt_bmod (x : Int64) : x.toInt.bmod 18446744073709551616 = x.toInt

@[simp]

theorem ISize.toInt_bmod_two_pow_numBits (x : ISize) : x.toInt.bmod (2 ^ System.Platform.numBits) = x.toInt

@[simp]

theorem Int8.toInt_bmod_65536 (x : Int8) : x.toInt.bmod 65536 = x.toInt

@[simp]

theorem Int8.toInt_bmod_4294967296 (x : Int8) : x.toInt.bmod 4294967296 = x.toInt

@[simp]

theorem Int16.toInt_bmod_4294967296 (x : Int16) : x.toInt.bmod 4294967296 = x.toInt

@[simp]

theorem Int8.toInt_bmod_18446744073709551616 (x : Int8) : x.toInt.bmod 18446744073709551616 = x.toInt

@[simp]

theorem Int16.toInt_bmod_18446744073709551616 (x : Int16) : x.toInt.bmod 18446744073709551616 = x.toInt

@[simp]

theorem Int32.toInt_bmod_18446744073709551616 (x : Int32) : x.toInt.bmod 18446744073709551616 = x.toInt

@[simp]

theorem ISize.toInt_bmod_18446744073709551616 (x : ISize) : x.toInt.bmod 18446744073709551616 = x.toInt

@[simp]

theorem Int8.toInt_bmod_two_pow_numBits (x : Int8) : x.toInt.bmod (2 ^ System.Platform.numBits) = x.toInt

@[simp]

theorem Int16.toInt_bmod_two_pow_numBits (x : Int16) : x.toInt.bmod (2 ^ System.Platform.numBits) = x.toInt

@[simp]

theorem Int32.toInt_bmod_two_pow_numBits (x : Int32) : x.toInt.bmod (2 ^ System.Platform.numBits) = x.toInt

@[simp]

theorem BitVec.ofInt_int8ToInt (x : Int8) : BitVec.ofInt 8 x.toInt = x.toBitVec

@[simp]

theorem BitVec.ofInt_int16ToInt (x : Int16) : BitVec.ofInt 16 x.toInt = x.toBitVec

@[simp]

theorem BitVec.ofInt_int32ToInt (x : Int32) : BitVec.ofInt 32 x.toInt = x.toBitVec

@[simp]

theorem BitVec.ofInt_int64ToInt (x : Int64) : BitVec.ofInt 64 x.toInt = x.toBitVec

@[simp]

theorem BitVec.ofInt_iSizeToInt (x : ISize) : BitVec.ofInt System.Platform.numBits x.toInt = x.toBitVec

@[simp]

theorem Int8.ofIntLE_toInt (x : Int8) : ofIntLE x.toInt ⋯ ⋯ = x

@[simp]

theorem Int16.ofIntLE_toInt (x : Int16) : ofIntLE x.toInt ⋯ ⋯ = x

@[simp]

theorem Int32.ofIntLE_toInt (x : Int32) : ofIntLE x.toInt ⋯ ⋯ = x

@[simp]

theorem Int64.ofIntLE_toInt (x : Int64) : ofIntLE x.toInt ⋯ ⋯ = x

@[simp]

theorem ISize.ofIntLE_toInt (x : ISize) : ofIntLE x.toInt ⋯ ⋯ = x

theorem Int8.ofIntLE_int16ToInt (x : Int16) {h₁ : minValue.toInt ≤ x.toInt} {h₂ : x.toInt ≤ maxValue.toInt} : ofIntLE x.toInt h₁ h₂ = x.toInt8

theorem Int8.ofIntLE_int32ToInt (x : Int32) {h₁ : minValue.toInt ≤ x.toInt} {h₂ : x.toInt ≤ maxValue.toInt} : ofIntLE x.toInt h₁ h₂ = x.toInt8

theorem Int8.ofIntLE_int64ToInt (x : Int64) {h₁ : minValue.toInt ≤ x.toInt} {h₂ : x.toInt ≤ maxValue.toInt} : ofIntLE x.toInt h₁ h₂ = x.toInt8

theorem Int8.ofIntLE_iSizeToInt (x : ISize) {h₁ : minValue.toInt ≤ x.toInt} {h₂ : x.toInt ≤ maxValue.toInt} : ofIntLE x.toInt h₁ h₂ = x.toInt8

@[simp]

theorem Int16.ofIntLE_int8ToInt (x : Int8) : ofIntLE x.toInt ⋯ ⋯ = x.toInt16

theorem Int16.ofIntLE_int32ToInt (x : Int32) {h₁ : minValue.toInt ≤ x.toInt} {h₂ : x.toInt ≤ maxValue.toInt} : ofIntLE x.toInt h₁ h₂ = x.toInt16

theorem Int16.ofIntLE_int64ToInt (x : Int64) {h₁ : minValue.toInt ≤ x.toInt} {h₂ : x.toInt ≤ maxValue.toInt} : ofIntLE x.toInt h₁ h₂ = x.toInt16

theorem Int16.ofIntLE_iSizeToInt (x : ISize) {h₁ : minValue.toInt ≤ x.toInt} {h₂ : x.toInt ≤ maxValue.toInt} : ofIntLE x.toInt h₁ h₂ = x.toInt16

@[simp]

theorem Int32.ofIntLE_int8ToInt (x : Int8) : ofIntLE x.toInt ⋯ ⋯ = x.toInt32

@[simp]

theorem Int32.ofIntLE_int16ToInt (x : Int16) : ofIntLE x.toInt ⋯ ⋯ = x.toInt32

theorem Int32.ofIntLE_int64ToInt (x : Int64) {h₁ : minValue.toInt ≤ x.toInt} {h₂ : x.toInt ≤ maxValue.toInt} : ofIntLE x.toInt h₁ h₂ = x.toInt32

theorem Int32.ofIntLE_iSizeToInt (x : ISize) {h₁ : minValue.toInt ≤ x.toInt} {h₂ : x.toInt ≤ maxValue.toInt} : ofIntLE x.toInt h₁ h₂ = x.toInt32

@[simp]

theorem Int64.ofIntLE_int8ToInt (x : Int8) : ofIntLE x.toInt ⋯ ⋯ = x.toInt64

@[simp]

theorem Int64.ofIntLE_int16ToInt (x : Int16) : ofIntLE x.toInt ⋯ ⋯ = x.toInt64

@[simp]

theorem Int64.ofIntLE_int32ToInt (x : Int32) : ofIntLE x.toInt ⋯ ⋯ = x.toInt64

@[simp]

theorem Int64.ofIntLE_iSizeToInt (x : ISize) : ofIntLE x.toInt ⋯ ⋯ = x.toInt64

@[simp]

theorem ISize.ofIntLE_int8ToInt (x : Int8) : ofIntLE x.toInt ⋯ ⋯ = x.toISize

@[simp]

theorem ISize.ofIntLE_int16ToInt (x : Int16) : ofIntLE x.toInt ⋯ ⋯ = x.toISize

@[simp]

theorem ISize.ofIntLE_int32ToInt (x : Int32) : ofIntLE x.toInt ⋯ ⋯ = x.toISize

theorem ISize.ofIntLE_int64ToInt (x : Int64) {h₁ : minValue.toInt ≤ x.toInt} {h₂ : x.toInt ≤ maxValue.toInt} : ofIntLE x.toInt h₁ h₂ = x.toISize

@[simp]

theorem Int8.ofInt_toInt (x : Int8) : ofInt x.toInt = x

@[simp]

theorem Int16.ofInt_toInt (x : Int16) : ofInt x.toInt = x

@[simp]

theorem Int32.ofInt_toInt (x : Int32) : ofInt x.toInt = x

@[simp]

theorem Int64.ofInt_toInt (x : Int64) : ofInt x.toInt = x

@[simp]

theorem ISize.ofInt_toInt (x : ISize) : ofInt x.toInt = x

@[simp]

theorem Int8.ofInt_int16ToInt (x : Int16) : ofInt x.toInt = x.toInt8

@[simp]

theorem Int8.ofInt_int32ToInt (x : Int32) : ofInt x.toInt = x.toInt8

@[simp]

theorem Int8.ofInt_int64ToInt (x : Int64) : ofInt x.toInt = x.toInt8

@[simp]

theorem Int8.ofInt_iSizeToInt (x : ISize) : ofInt x.toInt = x.toInt8

@[simp]

theorem Int16.ofInt_int8ToInt (x : Int8) : ofInt x.toInt = x.toInt16

@[simp]

theorem Int16.ofInt_int32ToInt (x : Int32) : ofInt x.toInt = x.toInt16

@[simp]

theorem Int16.ofInt_int64ToInt (x : Int64) : ofInt x.toInt = x.toInt16

@[simp]

theorem Int16.ofInt_iSizeToInt (x : ISize) : ofInt x.toInt = x.toInt16

@[simp]

theorem Int32.ofInt_int8ToInt (x : Int8) : ofInt x.toInt = x.toInt32

@[simp]

theorem Int32.ofInt_int16ToInt (x : Int16) : ofInt x.toInt = x.toInt32

@[simp]

theorem Int32.ofInt_int64ToInt (x : Int64) : ofInt x.toInt = x.toInt32

@[simp]

theorem Int32.ofInt_iSizeToInt (x : ISize) : ofInt x.toInt = x.toInt32

@[simp]

theorem Int64.ofInt_int8ToInt (x : Int8) : ofInt x.toInt = x.toInt64

@[simp]

theorem Int64.ofInt_int16ToInt (x : Int16) : ofInt x.toInt = x.toInt64

@[simp]

theorem Int64.ofInt_int32ToInt (x : Int32) : ofInt x.toInt = x.toInt64

@[simp]

theorem Int64.ofInt_iSizeToInt (x : ISize) : ofInt x.toInt = x.toInt64

@[simp]

theorem ISize.ofInt_int8ToInt (x : Int8) : ofInt x.toInt = x.toISize

@[simp]

theorem ISize.ofInt_int16ToInt (x : Int16) : ofInt x.toInt = x.toISize

@[simp]

theorem ISize.ofInt_int32ToInt (x : Int32) : ofInt x.toInt = x.toISize

@[simp]

theorem ISize.ofInt_int64ToInt (x : Int64) : ofInt x.toInt = x.toISize

@[simp]

theorem Int8.toInt_ofIntLE {x : Int} {h₁ : minValue.toInt ≤ x} {h₂ : x ≤ maxValue.toInt} : (ofIntLE x h₁ h₂).toInt = x

@[simp]

theorem Int16.toInt_ofIntLE {x : Int} {h₁ : minValue.toInt ≤ x} {h₂ : x ≤ maxValue.toInt} : (ofIntLE x h₁ h₂).toInt = x

@[simp]

theorem Int32.toInt_ofIntLE {x : Int} {h₁ : minValue.toInt ≤ x} {h₂ : x ≤ maxValue.toInt} : (ofIntLE x h₁ h₂).toInt = x

@[simp]

theorem Int64.toInt_ofIntLE {x : Int} {h₁ : minValue.toInt ≤ x} {h₂ : x ≤ maxValue.toInt} : (ofIntLE x h₁ h₂).toInt = x

@[simp]

theorem ISize.toInt_ofIntLE {x : Int} {h₁ : minValue.toInt ≤ x} {h₂ : x ≤ maxValue.toInt} : (ofIntLE x h₁ h₂).toInt = x

theorem Int8.ofIntLE_eq_ofIntClamp {x : Int} {h₁ : minValue.toInt ≤ x} {h₂ : x ≤ maxValue.toInt} : ofIntLE x h₁ h₂ = ofIntClamp x

theorem Int16.ofIntLE_eq_ofIntClamp {x : Int} {h₁ : minValue.toInt ≤ x} {h₂ : x ≤ maxValue.toInt} : ofIntLE x h₁ h₂ = ofIntClamp x

theorem Int32.ofIntLE_eq_ofIntClamp {x : Int} {h₁ : minValue.toInt ≤ x} {h₂ : x ≤ maxValue.toInt} : ofIntLE x h₁ h₂ = ofIntClamp x

theorem Int64.ofIntLE_eq_ofIntClamp {x : Int} {h₁ : minValue.toInt ≤ x} {h₂ : x ≤ maxValue.toInt} : ofIntLE x h₁ h₂ = ofIntClamp x

theorem ISize.ofIntLE_eq_ofIntClamp {x : Int} {h₁ : minValue.toInt ≤ x} {h₂ : x ≤ maxValue.toInt} : ofIntLE x h₁ h₂ = ofIntClamp x

theorem Int8.ofIntLE_eq_ofInt {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : ofIntLE n h₁ h₂ = ofInt n

theorem Int16.ofIntLE_eq_ofInt {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : ofIntLE n h₁ h₂ = ofInt n

theorem Int32.ofIntLE_eq_ofInt {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : ofIntLE n h₁ h₂ = ofInt n

theorem Int64.ofIntLE_eq_ofInt {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : ofIntLE n h₁ h₂ = ofInt n

theorem ISize.ofIntLE_eq_ofInt {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : ofIntLE n h₁ h₂ = ofInt n

theorem Int8.toInt_ofIntClamp {x : Int} (h₁ : minValue.toInt ≤ x) (h₂ : x ≤ maxValue.toInt) : (ofIntClamp x).toInt = x

theorem Int16.toInt_ofIntClamp {x : Int} (h₁ : minValue.toInt ≤ x) (h₂ : x ≤ maxValue.toInt) : (ofIntClamp x).toInt = x

theorem Int32.toInt_ofIntClamp {x : Int} (h₁ : minValue.toInt ≤ x) (h₂ : x ≤ maxValue.toInt) : (ofIntClamp x).toInt = x

theorem Int64.toInt_ofIntClamp {x : Int} (h₁ : minValue.toInt ≤ x) (h₂ : x ≤ maxValue.toInt) : (ofIntClamp x).toInt = x

theorem ISize.toInt_ofIntClamp {x : Int} (h₁ : minValue.toInt ≤ x) (h₂ : x ≤ maxValue.toInt) : (ofIntClamp x).toInt = x

@[simp]

theorem Int8.ofIntClamp_toInt (x : Int8) : ofIntClamp x.toInt = x

@[simp]

theorem Int16.ofIntClamp_toInt (x : Int16) : ofIntClamp x.toInt = x

@[simp]

theorem Int32.ofIntClamp_toInt (x : Int32) : ofIntClamp x.toInt = x

@[simp]

theorem Int64.ofIntClamp_toInt (x : Int64) : ofIntClamp x.toInt = x

@[simp]

theorem ISize.ofIntClamp_toInt (x : ISize) : ofIntClamp x.toInt = x

@[simp]

theorem Int16.ofIntClamp_int8ToInt (x : Int8) : ofIntClamp x.toInt = x.toInt16

@[simp]

theorem Int32.ofIntClamp_int8ToInt (x : Int8) : ofIntClamp x.toInt = x.toInt32

@[simp]

theorem Int64.ofIntClamp_int8ToInt (x : Int8) : ofIntClamp x.toInt = x.toInt64

@[simp]

theorem ISize.ofIntClamp_int8ToInt (x : Int8) : ofIntClamp x.toInt = x.toISize

@[simp]

theorem Int32.ofIntClamp_int16ToInt (x : Int16) : ofIntClamp x.toInt = x.toInt32

@[simp]

theorem Int64.ofIntClamp_int16ToInt (x : Int16) : ofIntClamp x.toInt = x.toInt64

@[simp]

theorem ISize.ofIntClamp_int16ToInt (x : Int16) : ofIntClamp x.toInt = x.toISize

@[simp]

theorem Int64.ofIntClamp_int32ToInt (x : Int32) : ofIntClamp x.toInt = x.toInt64

@[simp]

theorem ISize.ofIntClamp_int32ToInt (x : Int32) : ofIntClamp x.toInt = x.toISize

@[simp]

theorem Int64.ofIntClamp_iSizeToInt (x : ISize) : ofIntClamp x.toInt = x.toInt64

theorem Int8.le_iff_toInt_le {x y : Int8} : x ≤ y ↔ x.toInt ≤ y.toInt

theorem Int16.le_iff_toInt_le {x y : Int16} : x ≤ y ↔ x.toInt ≤ y.toInt

theorem Int32.le_iff_toInt_le {x y : Int32} : x ≤ y ↔ x.toInt ≤ y.toInt

theorem Int64.le_iff_toInt_le {x y : Int64} : x ≤ y ↔ x.toInt ≤ y.toInt

theorem ISize.le_iff_toInt_le {x y : ISize} : x ≤ y ↔ x.toInt ≤ y.toInt

theorem Int8.lt_iff_toInt_lt {x y : Int8} : x < y ↔ x.toInt < y.toInt

theorem Int16.lt_iff_toInt_lt {x y : Int16} : x < y ↔ x.toInt < y.toInt

theorem Int32.lt_iff_toInt_lt {x y : Int32} : x < y ↔ x.toInt < y.toInt

theorem Int64.lt_iff_toInt_lt {x y : Int64} : x < y ↔ x.toInt < y.toInt

theorem ISize.lt_iff_toInt_lt {x y : ISize} : x < y ↔ x.toInt < y.toInt

theorem Int8.cast_toNatClampNeg (x : Int8) (hx : 0 ≤ x) : ↑x.toNatClampNeg = x.toInt

theorem Int16.cast_toNatClampNeg (x : Int16) (hx : 0 ≤ x) : ↑x.toNatClampNeg = x.toInt

theorem Int32.cast_toNatClampNeg (x : Int32) (hx : 0 ≤ x) : ↑x.toNatClampNeg = x.toInt

theorem Int64.cast_toNatClampNeg (x : Int64) (hx : 0 ≤ x) : ↑x.toNatClampNeg = x.toInt

theorem ISize.cast_toNatClampNeg (x : ISize) (hx : 0 ≤ x) : ↑x.toNatClampNeg = x.toInt

theorem Int8.ofNat_toNatClampNeg (x : Int8) (hx : 0 ≤ x) : ofNat x.toNatClampNeg = x

theorem Int16.ofNat_toNatClampNeg (x : Int16) (hx : 0 ≤ x) : ofNat x.toNatClampNeg = x

theorem Int32.ofNat_toNatClampNeg (x : Int32) (hx : 0 ≤ x) : ofNat x.toNatClampNeg = x

theorem Int64.ofNat_toNatClampNeg (x : Int64) (hx : 0 ≤ x) : ofNat x.toNatClampNeg = x

theorem ISize.ofNat_toNatClampNeg (x : ISize) (hx : 0 ≤ x) : ofNat x.toNatClampNeg = x

theorem Int16.ofNat_int8ToNatClampNeg (x : Int8) (hx : 0 ≤ x) : ofNat x.toNatClampNeg = x.toInt16

theorem Int32.ofNat_int8ToNatClampNeg (x : Int8) (hx : 0 ≤ x) : ofNat x.toNatClampNeg = x.toInt32

theorem Int64.ofNat_int8ToNatClampNeg (x : Int8) (hx : 0 ≤ x) : ofNat x.toNatClampNeg = x.toInt64

theorem ISize.ofNat_int8ToNatClampNeg (x : Int8) (hx : 0 ≤ x) : ofNat x.toNatClampNeg = x.toISize

theorem Int32.ofNat_int16ToNatClampNeg (x : Int16) (hx : 0 ≤ x) : ofNat x.toNatClampNeg = x.toInt32

theorem Int64.ofNat_int16ToNatClampNeg (x : Int16) (hx : 0 ≤ x) : ofNat x.toNatClampNeg = x.toInt64

theorem ISize.ofNat_int16ToNatClampNeg (x : Int16) (hx : 0 ≤ x) : ofNat x.toNatClampNeg = x.toISize

theorem Int64.ofNat_int32ToNatClampNeg (x : Int32) (hx : 0 ≤ x) : ofNat x.toNatClampNeg = x.toInt64

theorem ISize.ofNat_int32ToNatClampNeg (x : Int32) (hx : 0 ≤ x) : ofNat x.toNatClampNeg = x.toISize

@[simp]

theorem Int8.toInt8_toInt16 (n : Int8) : n.toInt16.toInt8 = n

@[simp]

theorem Int8.toInt8_toInt32 (n : Int8) : n.toInt32.toInt8 = n

@[simp]

theorem Int8.toInt8_toInt64 (n : Int8) : n.toInt64.toInt8 = n

@[simp]

theorem Int8.toInt8_toISize (n : Int8) : n.toISize.toInt8 = n

@[simp]

theorem Int8.toInt16_toInt32 (n : Int8) : n.toInt32.toInt16 = n.toInt16

@[simp]

theorem Int8.toInt16_toInt64 (n : Int8) : n.toInt64.toInt16 = n.toInt16

@[simp]

theorem Int8.toInt16_toISize (n : Int8) : n.toISize.toInt16 = n.toInt16

@[simp]

theorem Int8.toInt32_toInt16 (n : Int8) : n.toInt16.toInt32 = n.toInt32

@[simp]

theorem Int8.toInt32_toInt64 (n : Int8) : n.toInt64.toInt32 = n.toInt32

@[simp]

theorem Int8.toInt32_toISize (n : Int8) : n.toISize.toInt32 = n.toInt32

@[simp]

theorem Int8.toInt64_toInt16 (n : Int8) : n.toInt16.toInt64 = n.toInt64

@[simp]

theorem Int8.toInt64_toInt32 (n : Int8) : n.toInt32.toInt64 = n.toInt64

@[simp]

theorem Int8.toInt64_toISize (n : Int8) : n.toISize.toInt64 = n.toInt64

@[simp]

theorem Int8.toISize_toInt16 (n : Int8) : n.toInt16.toISize = n.toISize

@[simp]

theorem Int8.toISize_toInt32 (n : Int8) : n.toInt32.toISize = n.toISize

@[simp]

theorem Int8.toISize_toInt64 (n : Int8) : n.toInt64.toISize = n.toISize

@[simp]

theorem Int16.toInt8_toInt32 (n : Int16) : n.toInt32.toInt8 = n.toInt8

@[simp]

theorem Int16.toInt8_toInt64 (n : Int16) : n.toInt64.toInt8 = n.toInt8

@[simp]

theorem Int16.toInt8_toISize (n : Int16) : n.toISize.toInt8 = n.toInt8

@[simp]

theorem Int16.toInt16_toInt32 (n : Int16) : n.toInt32.toInt16 = n

@[simp]

theorem Int16.toInt16_toInt64 (n : Int16) : n.toInt64.toInt16 = n

@[simp]

theorem Int16.toInt16_toISize (n : Int16) : n.toISize.toInt16 = n

@[simp]

theorem Int16.toInt32_toInt64 (n : Int16) : n.toInt64.toInt32 = n.toInt32

@[simp]

theorem Int16.toInt32_toISize (n : Int16) : n.toISize.toInt32 = n.toInt32

@[simp]

theorem Int16.toInt64_toInt32 (n : Int16) : n.toInt32.toInt64 = n.toInt64

@[simp]

theorem Int16.toInt64_toISize (n : Int16) : n.toISize.toInt64 = n.toInt64

@[simp]

theorem Int16.toISize_toInt32 (n : Int16) : n.toInt32.toISize = n.toISize

@[simp]

theorem Int16.toISize_toInt64 (n : Int16) : n.toInt64.toISize = n.toISize

@[simp]

theorem Int32.toInt8_toInt16 (n : Int32) : n.toInt16.toInt8 = n.toInt8

@[simp]

theorem Int32.toInt8_toInt64 (n : Int32) : n.toInt64.toInt8 = n.toInt8

@[simp]

theorem Int32.toInt8_toISize (n : Int32) : n.toISize.toInt8 = n.toInt8

@[simp]

theorem Int32.toInt16_toInt64 (n : Int32) : n.toInt64.toInt16 = n.toInt16

@[simp]

theorem Int32.toInt16_toISize (n : Int32) : n.toISize.toInt16 = n.toInt16

@[simp]

theorem Int32.toInt32_toInt64 (n : Int32) : n.toInt64.toInt32 = n

@[simp]

theorem Int32.toInt32_toISize (n : Int32) : n.toISize.toInt32 = n

@[simp]

theorem Int32.toInt64_toISize (n : Int32) : n.toISize.toInt64 = n.toInt64

@[simp]

theorem Int32.toISize_toInt64 (n : Int32) : n.toInt64.toISize = n.toISize

@[simp]

theorem Int64.toInt8_toInt16 (n : Int64) : n.toInt16.toInt8 = n.toInt8

@[simp]

theorem Int64.toInt8_toInt32 (n : Int64) : n.toInt32.toInt8 = n.toInt8

@[simp]

theorem Int64.toInt8_toISize (n : Int64) : n.toISize.toInt8 = n.toInt8

@[simp]

theorem Int64.toInt16_toInt32 (n : Int64) : n.toInt32.toInt16 = n.toInt16

@[simp]

theorem Int64.toInt16_toISize (n : Int64) : n.toISize.toInt16 = n.toInt16

@[simp]

theorem Int64.toInt32_toISize (n : Int64) : n.toISize.toInt32 = n.toInt32

@[simp]

theorem ISize.toInt8_toInt16 (n : ISize) : n.toInt16.toInt8 = n.toInt8

@[simp]

theorem ISize.toInt8_toInt32 (n : ISize) : n.toInt32.toInt8 = n.toInt8

@[simp]

theorem ISize.toInt8_toInt64 (n : ISize) : n.toInt64.toInt8 = n.toInt8

@[simp]

theorem ISize.toInt16_toInt32 (n : ISize) : n.toInt32.toInt16 = n.toInt16

@[simp]

theorem ISize.toInt16_toInt64 (n : ISize) : n.toInt64.toInt16 = n.toInt16

@[simp]

theorem ISize.toInt32_toInt64 (n : ISize) : n.toInt64.toInt32 = n.toInt32

@[simp]

theorem ISize.toISize_toInt64 (n : ISize) : n.toInt64.toISize = n

theorem UInt8.toInt8_ofNatLT {n : Nat} (hn : n < size) : (ofNatLT n hn).toInt8 = Int8.ofNat n

theorem UInt16.toInt16_ofNatLT {n : Nat} (hn : n < size) : (ofNatLT n hn).toInt16 = Int16.ofNat n

theorem UInt32.toInt32_ofNatLT {n : Nat} (hn : n < size) : (ofNatLT n hn).toInt32 = Int32.ofNat n

theorem UInt64.toInt64_ofNatLT {n : Nat} (hn : n < size) : (ofNatLT n hn).toInt64 = Int64.ofNat n

theorem USize.toISize_ofNatLT {n : Nat} (hn : n < size) : (ofNatLT n hn).toISize = ISize.ofNat n

@[simp]

theorem UInt8.toInt8_ofNat' {n : Nat} : (ofNat n).toInt8 = Int8.ofNat n

@[simp]

theorem UInt16.toInt16_ofNat' {n : Nat} : (ofNat n).toInt16 = Int16.ofNat n

@[simp]

theorem UInt32.toInt32_ofNat' {n : Nat} : (ofNat n).toInt32 = Int32.ofNat n

@[simp]

theorem UInt64.toInt64_ofNat' {n : Nat} : (ofNat n).toInt64 = Int64.ofNat n

@[simp]

theorem USize.toISize_ofNat' {n : Nat} : (ofNat n).toISize = ISize.ofNat n

@[simp]

theorem UInt8.toInt8_ofNat {n : Nat} : (OfNat.ofNat n).toInt8 = OfNat.ofNat n

@[simp]

theorem UInt16.toInt16_ofNat {n : Nat} : (OfNat.ofNat n).toInt16 = OfNat.ofNat n

@[simp]

theorem UInt32.toInt32_ofNat {n : Nat} : (OfNat.ofNat n).toInt32 = OfNat.ofNat n

@[simp]

theorem UInt64.toInt64_ofNat {n : Nat} : (OfNat.ofNat n).toInt64 = OfNat.ofNat n

@[simp]

theorem USize.toISize_ofNat {n : Nat} : (OfNat.ofNat n).toISize = OfNat.ofNat n

@[simp]

theorem UInt8.toInt8_ofBitVec (b : BitVec 8) : { toBitVec := b }.toInt8 = Int8.ofBitVec b

@[simp]

theorem UInt16.toInt16_ofBitVec (b : BitVec 16) : { toBitVec := b }.toInt16 = Int16.ofBitVec b

@[simp]

theorem UInt32.toInt32_ofBitVec (b : BitVec 32) : { toBitVec := b }.toInt32 = Int32.ofBitVec b

@[simp]

theorem UInt64.toInt64_ofBitVec (b : BitVec 64) : { toBitVec := b }.toInt64 = Int64.ofBitVec b

@[simp]

theorem USize.toISize_ofBitVec (b : BitVec System.Platform.numBits) : { toBitVec := b }.toISize = ISize.ofBitVec b

@[simp]

theorem Int8.toBitVec_ofBitVec (b : BitVec 8) : (ofBitVec b).toBitVec = b

@[simp]

theorem Int16.toBitVec_ofBitVec (b : BitVec 16) : (ofBitVec b).toBitVec = b

@[simp]

theorem Int32.toBitVec_ofBitVec (b : BitVec 32) : (ofBitVec b).toBitVec = b

@[simp]

theorem Int64.toBitVec_ofBitVec (b : BitVec 64) : (ofBitVec b).toBitVec = b

@[simp]

theorem ISize.toBitVec_ofBitVec (b : BitVec System.Platform.numBits) : (ofBitVec b).toBitVec = b

theorem Int8.toBitVec_ofIntClamp {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntClamp n).toBitVec = BitVec.ofInt 8 n

theorem Int16.toBitVec_ofIntClamp {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntClamp n).toBitVec = BitVec.ofInt 16 n

theorem Int32.toBitVec_ofIntClamp {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntClamp n).toBitVec = BitVec.ofInt 32 n

theorem Int64.toBitVec_ofIntClamp {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntClamp n).toBitVec = BitVec.ofInt 64 n

theorem ISize.toBitVec_ofIntClamp {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntClamp n).toBitVec = BitVec.ofInt System.Platform.numBits n

@[simp]

theorem Int8.toInt_ofBitVec (b : BitVec 8) : (ofBitVec b).toInt = b.toInt

@[simp]

theorem Int16.toInt_ofBitVec (b : BitVec 16) : (ofBitVec b).toInt = b.toInt

@[simp]

theorem Int32.toInt_ofBitVec (b : BitVec 32) : (ofBitVec b).toInt = b.toInt

@[simp]

theorem Int64.toInt_ofBitVec (b : BitVec 64) : (ofBitVec b).toInt = b.toInt

@[simp]

theorem ISize.toInt_ofBitVec (b : BitVec System.Platform.numBits) : (ofBitVec b).toInt = b.toInt

@[simp]

theorem Int8.toNatClampNeg_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntLE n h₁ h₂).toNatClampNeg = n.toNat

@[simp]

theorem Int16.toNatClampNeg_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntLE n h₁ h₂).toNatClampNeg = n.toNat

@[simp]

theorem Int32.toNatClampNeg_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntLE n h₁ h₂).toNatClampNeg = n.toNat

@[simp]

theorem Int64.toNatClampNeg_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntLE n h₁ h₂).toNatClampNeg = n.toNat

@[simp]

theorem ISize.toNatClampNeg_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntLE n h₁ h₂).toNatClampNeg = n.toNat

@[simp]

theorem Int8.toNatClampNeg_ofBitVec (b : BitVec 8) : (ofBitVec b).toNatClampNeg = b.toInt.toNat

@[simp]

theorem Int16.toNatClampNeg_ofBitVec (b : BitVec 16) : (ofBitVec b).toNatClampNeg = b.toInt.toNat

@[simp]

theorem Int32.toNatClampNeg_ofBitVec (b : BitVec 32) : (ofBitVec b).toNatClampNeg = b.toInt.toNat

@[simp]

theorem Int64.toNatClampNeg_ofBitVec (b : BitVec 64) : (ofBitVec b).toNatClampNeg = b.toInt.toNat

@[simp]

theorem ISize.toNatClampNeg_ofBitVec (b : BitVec System.Platform.numBits) : (ofBitVec b).toNatClampNeg = b.toInt.toNat

theorem Int8.toNatClampNeg_ofInt_of_le {n : Int} (h₁ : -2 ^ 7 ≤ n) (h₂ : n < 2 ^ 7) : (ofInt n).toNatClampNeg = n.toNat

theorem Int16.toNatClampNeg_ofInt_of_le {n : Int} (h₁ : -2 ^ 15 ≤ n) (h₂ : n < 2 ^ 15) : (ofInt n).toNatClampNeg = n.toNat

theorem Int32.toNatClampNeg_ofInt_of_le {n : Int} (h₁ : -2 ^ 31 ≤ n) (h₂ : n < 2 ^ 31) : (ofInt n).toNatClampNeg = n.toNat

theorem Int64.toNatClampNeg_ofInt_of_le {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) : (ofInt n).toNatClampNeg = n.toNat

theorem ISize.toNatClampNeg_ofInt_of_le {n : Int} (h₁ : -2 ^ 31 ≤ n) (h₂ : n < 2 ^ 31) : (ofInt n).toNatClampNeg = n.toNat

theorem ISize.toNatClampNeg_ofInt_of_two_pow_numBits {n : Int} (h₁ : -2 ^ (System.Platform.numBits - 1) ≤ n) (h₂ : n < 2 ^ (System.Platform.numBits - 1)) : (ofInt n).toNatClampNeg = n.toNat

theorem Int8.toNatClampNeg_ofIntClamp_of_lt {n : Int} (h₁ : n < 2 ^ 7) : (ofIntClamp n).toNatClampNeg = n.toNat

theorem Int16.toNatClampNeg_ofIntClamp_of_lt {n : Int} (h₁ : n < 2 ^ 15) : (ofIntClamp n).toNatClampNeg = n.toNat

theorem Int32.toNatClampNeg_ofIntClamp_of_lt {n : Int} (h₁ : n < 2 ^ 31) : (ofIntClamp n).toNatClampNeg = n.toNat

theorem Int64.toNatClampNeg_ofIntClamp_of_lt {n : Int} (h₁ : n < 2 ^ 63) : (ofIntClamp n).toNatClampNeg = n.toNat

theorem ISize.toNatClampNeg_ofIntClamp_of_lt_two_pow_numBits {n : Int} (h₁ : n < 2 ^ (System.Platform.numBits - 1)) : (ofIntClamp n).toNatClampNeg = n.toNat

theorem ISize.toNatClampNeg_ofIntClamp_of_lt {n : Int} (h₁ : n < 2 ^ 31) : (ofIntClamp n).toNatClampNeg = n.toNat

@[simp]

theorem Int8.toUInt8_ofBitVec (b : BitVec 8) : (ofBitVec b).toUInt8 = { toBitVec := b }

@[simp]

theorem Int16.toUInt16_ofBitVec (b : BitVec 16) : (ofBitVec b).toUInt16 = { toBitVec := b }

@[simp]

theorem Int32.toUInt32_ofBitVec (b : BitVec 32) : (ofBitVec b).toUInt32 = { toBitVec := b }

@[simp]

theorem Int64.toUInt64_ofBitVec (b : BitVec 64) : (ofBitVec b).toUInt64 = { toBitVec := b }

@[simp]

theorem ISize.toUSize_ofBitVec (b : BitVec System.Platform.numBits) : (ofBitVec b).toUSize = { toBitVec := b }

@[simp]

theorem Int8.toUInt8_ofNat' {n : Nat} : (ofNat n).toUInt8 = UInt8.ofNat n

@[simp]

theorem Int16.toUInt16_ofNat' {n : Nat} : (ofNat n).toUInt16 = UInt16.ofNat n

@[simp]

theorem Int32.toUInt32_ofNat' {n : Nat} : (ofNat n).toUInt32 = UInt32.ofNat n

@[simp]

theorem Int64.toUInt64_ofNat' {n : Nat} : (ofNat n).toUInt64 = UInt64.ofNat n

@[simp]

theorem ISize.toUSize_ofNat' {n : Nat} : (ofNat n).toUSize = USize.ofNat n

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Int64.toUInt64_ofNat {n : Nat} : toUInt64 (OfNat.ofNat n) = OfNat.ofNat n

@[simp]

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

theorem Int16.toInt8_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntLE n h₁ h₂).toInt8 = Int8.ofInt n

theorem Int32.toInt8_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntLE n h₁ h₂).toInt8 = Int8.ofInt n

theorem Int64.toInt8_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntLE n h₁ h₂).toInt8 = Int8.ofInt n

theorem ISize.toInt8_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntLE n h₁ h₂).toInt8 = Int8.ofInt n

@[simp]

theorem Int16.toInt8_ofBitVec (b : BitVec 16) : (ofBitVec b).toInt8 = Int8.ofBitVec (BitVec.signExtend 8 b)

@[simp]

theorem Int32.toInt8_ofBitVec (b : BitVec 32) : (ofBitVec b).toInt8 = Int8.ofBitVec (BitVec.signExtend 8 b)

@[simp]

theorem Int64.toInt8_ofBitVec (b : BitVec 64) : (ofBitVec b).toInt8 = Int8.ofBitVec (BitVec.signExtend 8 b)

@[simp]

theorem ISize.toInt8_ofBitVec (b : BitVec System.Platform.numBits) : (ofBitVec b).toInt8 = Int8.ofBitVec (BitVec.signExtend 8 b)

@[simp]

theorem Int16.toInt8_ofNat' {n : Nat} : (ofNat n).toInt8 = Int8.ofNat n

@[simp]

theorem Int32.toInt8_ofNat' {n : Nat} : (ofNat n).toInt8 = Int8.ofNat n

@[simp]

theorem Int64.toInt8_ofNat' {n : Nat} : (ofNat n).toInt8 = Int8.ofNat n

@[simp]

theorem ISize.toInt8_ofNat' {n : Nat} : (ofNat n).toInt8 = Int8.ofNat n

@[simp]

theorem Int16.toInt8_ofInt {n : Int} : (ofInt n).toInt8 = Int8.ofInt n

@[simp]

theorem Int32.toInt8_ofInt {n : Int} : (ofInt n).toInt8 = Int8.ofInt n

@[simp]

theorem Int64.toInt8_ofInt {n : Int} : (ofInt n).toInt8 = Int8.ofInt n

@[simp]

theorem ISize.toInt8_ofInt {n : Int} : (ofInt n).toInt8 = Int8.ofInt n

@[simp]

theorem Int16.toInt8_ofNat {n : Nat} : (OfNat.ofNat n).toInt8 = OfNat.ofNat n

@[simp]

theorem Int32.toInt8_ofNat {n : Nat} : (OfNat.ofNat n).toInt8 = OfNat.ofNat n

@[simp]

theorem Int64.toInt8_ofNat {n : Nat} : (OfNat.ofNat n).toInt8 = OfNat.ofNat n

@[simp]

theorem ISize.toInt8_ofNat {n : Nat} : (OfNat.ofNat n).toInt8 = OfNat.ofNat n

theorem Int16.toInt8_ofIntClamp {n : Int} (h₁ : -2 ^ 15 ≤ n) (h₂ : n < 2 ^ 15) : (ofIntClamp n).toInt8 = Int8.ofInt n

theorem Int32.toInt8_ofIntClamp {n : Int} (h₁ : -2 ^ 31 ≤ n) (h₂ : n < 2 ^ 31) : (ofIntClamp n).toInt8 = Int8.ofInt n

theorem Int64.toInt8_ofIntClamp {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) : (ofIntClamp n).toInt8 = Int8.ofInt n

theorem ISize.toInt8_ofIntClamp {n : Int} (h₁ : -2 ^ (System.Platform.numBits - 1) ≤ n) (h₂ : n < 2 ^ (System.Platform.numBits - 1)) : (ofIntClamp n).toInt8 = Int8.ofInt n

theorem Int32.toInt16_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntLE n h₁ h₂).toInt16 = Int16.ofInt n

theorem Int64.toInt16_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntLE n h₁ h₂).toInt16 = Int16.ofInt n

theorem ISize.toInt16_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntLE n h₁ h₂).toInt16 = Int16.ofInt n

@[simp]

theorem Int32.toInt16_ofBitVec (b : BitVec 32) : (ofBitVec b).toInt16 = Int16.ofBitVec (BitVec.signExtend 16 b)

@[simp]

theorem Int64.toInt16_ofBitVec (b : BitVec 64) : (ofBitVec b).toInt16 = Int16.ofBitVec (BitVec.signExtend 16 b)

@[simp]

theorem ISize.toInt16_ofBitVec (b : BitVec System.Platform.numBits) : (ofBitVec b).toInt16 = Int16.ofBitVec (BitVec.signExtend 16 b)

@[simp]

theorem Int32.toInt16_ofNat' {n : Nat} : (ofNat n).toInt16 = Int16.ofNat n

@[simp]

theorem Int64.toInt16_ofNat' {n : Nat} : (ofNat n).toInt16 = Int16.ofNat n

@[simp]

theorem ISize.toInt16_ofNat' {n : Nat} : (ofNat n).toInt16 = Int16.ofNat n

@[simp]

theorem Int32.toInt16_ofInt {n : Int} : (ofInt n).toInt16 = Int16.ofInt n

@[simp]

theorem Int64.toInt16_ofInt {n : Int} : (ofInt n).toInt16 = Int16.ofInt n

@[simp]

theorem ISize.toInt16_ofInt {n : Int} : (ofInt n).toInt16 = Int16.ofInt n

@[simp]

theorem Int32.toInt16_ofNat {n : Nat} : (OfNat.ofNat n).toInt16 = OfNat.ofNat n

@[simp]

theorem Int64.toInt16_ofNat {n : Nat} : (OfNat.ofNat n).toInt16 = OfNat.ofNat n

@[simp]

theorem ISize.toInt16_ofNat {n : Nat} : (OfNat.ofNat n).toInt16 = OfNat.ofNat n

theorem Int32.toInt16_ofIntClamp {n : Int} (h₁ : -2 ^ 31 ≤ n) (h₂ : n < 2 ^ 31) : (ofIntClamp n).toInt16 = Int16.ofInt n

theorem Int64.toInt16_ofIntClamp {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) : (ofIntClamp n).toInt16 = Int16.ofInt n

theorem ISize.toInt16_ofIntClamp {n : Int} (h₁ : -2 ^ (System.Platform.numBits - 1) ≤ n) (h₂ : n < 2 ^ (System.Platform.numBits - 1)) : (ofIntClamp n).toInt16 = Int16.ofInt n

theorem Int64.toInt32_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntLE n h₁ h₂).toInt32 = Int32.ofInt n

theorem ISize.toInt32_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntLE n h₁ h₂).toInt32 = Int32.ofInt n

@[simp]

theorem Int64.toInt32_ofBitVec (b : BitVec 64) : (ofBitVec b).toInt32 = Int32.ofBitVec (BitVec.signExtend 32 b)

@[simp]

theorem ISize.toInt32_ofBitVec (b : BitVec System.Platform.numBits) : (ofBitVec b).toInt32 = Int32.ofBitVec (BitVec.signExtend 32 b)

@[simp]

theorem Int64.toInt32_ofNat' {n : Nat} : (ofNat n).toInt32 = Int32.ofNat n

@[simp]

theorem ISize.toInt32_ofNat' {n : Nat} : (ofNat n).toInt32 = Int32.ofNat n

@[simp]

theorem Int64.toInt32_ofInt {n : Int} : (ofInt n).toInt32 = Int32.ofInt n

@[simp]

theorem ISize.toInt32_ofInt {n : Int} : (ofInt n).toInt32 = Int32.ofInt n

@[simp]

theorem Int64.toInt32_ofNat {n : Nat} : (OfNat.ofNat n).toInt32 = OfNat.ofNat n

@[simp]

theorem ISize.toInt32_ofNat {n : Nat} : (OfNat.ofNat n).toInt32 = OfNat.ofNat n

theorem Int64.toInt32_ofIntClamp {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) : (ofIntClamp n).toInt32 = Int32.ofInt n

theorem ISize.toInt32_ofIntClamp {n : Int} (h₁ : -2 ^ (System.Platform.numBits - 1) ≤ n) (h₂ : n < 2 ^ (System.Platform.numBits - 1)) : (ofIntClamp n).toInt32 = Int32.ofInt n

theorem Int64.toISize_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntLE n h₁ h₂).toISize = ISize.ofInt n

@[simp]

theorem Int64.toISize_ofBitVec (b : BitVec 64) : (ofBitVec b).toISize = ISize.ofBitVec (BitVec.signExtend System.Platform.numBits b)

@[simp]

theorem Int64.toISize_ofNat' {n : Nat} : (ofNat n).toISize = ISize.ofNat n

@[simp]

theorem Int64.toISize_ofInt {n : Int} : (ofInt n).toISize = ISize.ofInt n

@[simp]

theorem Int64.toISize_ofNat {n : Nat} : (OfNat.ofNat n).toISize = OfNat.ofNat n

theorem Int64.toISize_ofIntClamp {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) : (ofIntClamp n).toISize = ISize.ofInt n

@[simp]

theorem Int8.toBitVec_minValue : minValue.toBitVec = BitVec.intMin 8

@[simp]

theorem Int16.toBitVec_minValue : minValue.toBitVec = BitVec.intMin 16

@[simp]

theorem Int32.toBitVec_minValue : minValue.toBitVec = BitVec.intMin 32

@[simp]

theorem Int64.toBitVec_minValue : minValue.toBitVec = BitVec.intMin 64

@[simp]

theorem ISize.toBitVec_minValue : minValue.toBitVec = BitVec.intMin System.Platform.numBits

@[simp]

theorem Int8.toBitVec_maxValue : maxValue.toBitVec = BitVec.intMax 8

@[simp]

theorem Int16.toBitVec_maxValue : maxValue.toBitVec = BitVec.intMax 16

@[simp]

theorem Int32.toBitVec_maxValue : maxValue.toBitVec = BitVec.intMax 32

@[simp]

theorem Int64.toBitVec_maxValue : maxValue.toBitVec = BitVec.intMax 64

@[simp]

theorem ISize.toBitVec_maxValue : maxValue.toBitVec = BitVec.intMax System.Platform.numBits

@[simp]

theorem Int16.toInt8_neg (x : Int16) : (-x).toInt8 = -x.toInt8

@[simp]

theorem Int32.toInt8_neg (x : Int32) : (-x).toInt8 = -x.toInt8

@[simp]

theorem Int64.toInt8_neg (x : Int64) : (-x).toInt8 = -x.toInt8

@[simp]

theorem ISize.toInt8_neg (x : ISize) : (-x).toInt8 = -x.toInt8

@[simp]

theorem Int32.toInt16_neg (x : Int32) : (-x).toInt16 = -x.toInt16

@[simp]

theorem Int64.toInt16_neg (x : Int64) : (-x).toInt16 = -x.toInt16

@[simp]

theorem ISize.toInt16_neg (x : ISize) : (-x).toInt16 = -x.toInt16

@[simp]

theorem Int64.toInt32_neg (x : Int64) : (-x).toInt32 = -x.toInt32

@[simp]

theorem ISize.toInt32_neg (x : ISize) : (-x).toInt32 = -x.toInt32

@[simp]

theorem Int64.toISize_neg (x : Int64) : (-x).toISize = -x.toISize

@[simp]

theorem Int8.toInt16_neg_of_ne {x : Int8} (hx : x ≠ -128) : (-x).toInt16 = -x.toInt16

@[simp]

theorem Int8.toInt32_neg_of_ne {x : Int8} (hx : x ≠ -128) : (-x).toInt32 = -x.toInt32

@[simp]

theorem Int16.toInt32_neg_of_ne {x : Int16} (hx : x ≠ -32768) : (-x).toInt32 = -x.toInt32

@[simp]

theorem Int8.toISize_neg_of_ne {x : Int8} (hx : x ≠ -128) : (-x).toISize = -x.toISize

@[simp]

theorem Int16.toISize_neg_of_ne {x : Int16} (hx : x ≠ -32768) : (-x).toISize = -x.toISize

@[simp]

theorem Int32.toISize_neg_of_ne {x : Int32} (hx : x ≠ -2147483648) : (-x).toISize = -x.toISize

@[simp]

theorem Int8.toInt64_neg_of_ne {x : Int8} (hx : x ≠ -128) : (-x).toInt64 = -x.toInt64

@[simp]

theorem Int16.toInt64_neg_of_ne {x : Int16} (hx : x ≠ -32768) : (-x).toInt64 = -x.toInt64

@[simp]

theorem Int32.toInt64_neg_of_ne {x : Int32} (hx : x ≠ -2147483648) : (-x).toInt64 = -x.toInt64

@[simp]

theorem ISize.toInt64_neg_of_ne {x : ISize} (hx : x ≠ minValue) : (-x).toInt64 = -x.toInt64

theorem Int8.toInt16_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntLE n h₁ h₂).toInt16 = Int16.ofIntLE n ⋯ ⋯

theorem Int8.toInt32_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntLE n h₁ h₂).toInt32 = Int32.ofIntLE n ⋯ ⋯

theorem Int8.toInt64_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntLE n h₁ h₂).toInt64 = Int64.ofIntLE n ⋯ ⋯

theorem Int8.toISize_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntLE n h₁ h₂).toISize = ISize.ofIntLE n ⋯ ⋯

@[simp]

theorem Int8.toInt16_ofBitVec (b : BitVec 8) : (ofBitVec b).toInt16 = Int16.ofBitVec (BitVec.signExtend 16 b)

@[simp]

theorem Int8.toInt32_ofBitVec (b : BitVec 8) : (ofBitVec b).toInt32 = Int32.ofBitVec (BitVec.signExtend 32 b)

@[simp]

theorem Int8.toInt64_ofBitVec (b : BitVec 8) : (ofBitVec b).toInt64 = Int64.ofBitVec (BitVec.signExtend 64 b)

@[simp]

theorem Int8.toISize_ofBitVec (b : BitVec 8) : (ofBitVec b).toISize = ISize.ofBitVec (BitVec.signExtend System.Platform.numBits b)

@[simp]

theorem Int8.toInt16_ofInt {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofInt n).toInt16 = Int16.ofInt n

@[simp]

theorem Int8.toInt32_ofInt {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofInt n).toInt32 = Int32.ofInt n

@[simp]

theorem Int8.toInt64_ofInt {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofInt n).toInt64 = Int64.ofInt n

@[simp]

theorem Int8.toISize_ofInt {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofInt n).toISize = ISize.ofInt n

@[simp]

theorem Int8.toInt16_ofNat' {n : Nat} (h : ↑n ≤ maxValue.toInt) : (ofNat n).toInt16 = Int16.ofNat n

@[simp]

theorem Int8.toInt32_ofNat' {n : Nat} (h : ↑n ≤ maxValue.toInt) : (ofNat n).toInt32 = Int32.ofNat n

@[simp]

theorem Int8.toInt64_ofNat' {n : Nat} (h : ↑n ≤ maxValue.toInt) : (ofNat n).toInt64 = Int64.ofNat n

@[simp]

theorem Int8.toISize_ofNat' {n : Nat} (h : ↑n ≤ maxValue.toInt) : (ofNat n).toISize = ISize.ofNat n

@[simp]

theorem Int8.toInt16_ofNat {n : Nat} (h : n ≤ 127) : (OfNat.ofNat n).toInt16 = OfNat.ofNat n

@[simp]

theorem Int8.toInt32_ofNat {n : Nat} (h : n ≤ 127) : (OfNat.ofNat n).toInt32 = OfNat.ofNat n

@[simp]

theorem Int8.toInt64_ofNat {n : Nat} (h : n ≤ 127) : (OfNat.ofNat n).toInt64 = OfNat.ofNat n

@[simp]

theorem Int8.toISize_ofNat {n : Nat} (h : n ≤ 127) : (OfNat.ofNat n).toISize = OfNat.ofNat n

theorem Int16.toInt32_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntLE n h₁ h₂).toInt32 = Int32.ofIntLE n ⋯ ⋯

theorem Int16.toInt64_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntLE n h₁ h₂).toInt64 = Int64.ofIntLE n ⋯ ⋯

theorem Int16.toISize_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntLE n h₁ h₂).toISize = ISize.ofIntLE n ⋯ ⋯

@[simp]

theorem Int16.toInt32_ofBitVec (b : BitVec 16) : (ofBitVec b).toInt32 = Int32.ofBitVec (BitVec.signExtend 32 b)

@[simp]

theorem Int16.toInt64_ofBitVec (b : BitVec 16) : (ofBitVec b).toInt64 = Int64.ofBitVec (BitVec.signExtend 64 b)

@[simp]

theorem Int16.toISize_ofBitVec (b : BitVec 16) : (ofBitVec b).toISize = ISize.ofBitVec (BitVec.signExtend System.Platform.numBits b)

@[simp]

theorem Int16.toInt32_ofInt {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofInt n).toInt32 = Int32.ofInt n

@[simp]

theorem Int16.toInt64_ofInt {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofInt n).toInt64 = Int64.ofInt n

@[simp]

theorem Int16.toISize_ofInt {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofInt n).toISize = ISize.ofInt n

@[simp]

theorem Int16.toInt32_ofNat' {n : Nat} (h : ↑n ≤ maxValue.toInt) : (ofNat n).toInt32 = Int32.ofNat n

@[simp]

theorem Int16.toInt64_ofNat' {n : Nat} (h : ↑n ≤ maxValue.toInt) : (ofNat n).toInt64 = Int64.ofNat n

@[simp]

theorem Int16.toISize_ofNat' {n : Nat} (h : ↑n ≤ maxValue.toInt) : (ofNat n).toISize = ISize.ofNat n

@[simp]

theorem Int16.toInt32_ofNat {n : Nat} (h : n ≤ 32767) : (OfNat.ofNat n).toInt32 = OfNat.ofNat n

@[simp]

theorem Int16.toInt64_ofNat {n : Nat} (h : n ≤ 32767) : (OfNat.ofNat n).toInt64 = OfNat.ofNat n

@[simp]

theorem Int16.toISize_ofNat {n : Nat} (h : n ≤ 32767) : (OfNat.ofNat n).toISize = OfNat.ofNat n

theorem Int32.toInt64_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntLE n h₁ h₂).toInt64 = Int64.ofIntLE n ⋯ ⋯

theorem Int32.toISize_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntLE n h₁ h₂).toISize = ISize.ofIntLE n ⋯ ⋯

@[simp]

theorem Int32.toInt64_ofBitVec (b : BitVec 32) : (ofBitVec b).toInt64 = Int64.ofBitVec (BitVec.signExtend 64 b)

@[simp]

theorem Int32.toISize_ofBitVec (b : BitVec 32) : (ofBitVec b).toISize = ISize.ofBitVec (BitVec.signExtend System.Platform.numBits b)

@[simp]

theorem Int32.toInt64_ofInt {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofInt n).toInt64 = Int64.ofInt n

@[simp]

theorem Int32.toISize_ofInt {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofInt n).toISize = ISize.ofInt n

@[simp]

theorem Int32.toInt64_ofNat' {n : Nat} (h : ↑n ≤ maxValue.toInt) : (ofNat n).toInt64 = Int64.ofNat n

@[simp]

theorem Int32.toISize_ofNat' {n : Nat} (h : ↑n ≤ maxValue.toInt) : (ofNat n).toISize = ISize.ofNat n

@[simp]

theorem Int32.toInt64_ofNat {n : Nat} (h : n ≤ 2147483647) : (OfNat.ofNat n).toInt64 = OfNat.ofNat n

@[simp]

theorem Int32.toISize_ofNat {n : Nat} (h : n ≤ 2147483647) : (OfNat.ofNat n).toISize = OfNat.ofNat n

theorem ISize.toInt64_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntLE n h₁ h₂).toInt64 = Int64.ofIntLE n ⋯ ⋯

@[simp]

theorem ISize.toInt64_ofBitVec (b : BitVec System.Platform.numBits) : (ofBitVec b).toInt64 = Int64.ofBitVec (BitVec.signExtend 64 b)

@[simp]

theorem ISize.toInt64_ofInt {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofInt n).toInt64 = Int64.ofInt n

@[simp]

theorem ISize.toInt64_ofNat' {n : Nat} (h : ↑n ≤ maxValue.toInt) : (ofNat n).toInt64 = Int64.ofNat n

@[simp]

theorem ISize.toInt64_ofNat {n : Nat} (h : n ≤ 2147483647) : (OfNat.ofNat n).toInt64 = OfNat.ofNat n

@[simp]

theorem Int8.ofIntLE_bitVecToInt (n : BitVec 8) : ofIntLE n.toInt ⋯ ⋯ = ofBitVec n

@[simp]

theorem Int16.ofIntLE_bitVecToInt (n : BitVec 16) : ofIntLE n.toInt ⋯ ⋯ = ofBitVec n

@[simp]

theorem Int32.ofIntLE_bitVecToInt (n : BitVec 32) : ofIntLE n.toInt ⋯ ⋯ = ofBitVec n

@[simp]

theorem Int64.ofIntLE_bitVecToInt (n : BitVec 64) : ofIntLE n.toInt ⋯ ⋯ = ofBitVec n

@[simp]

theorem ISize.ofIntLE_bitVecToInt (n : BitVec System.Platform.numBits) : ofIntLE n.toInt ⋯ ⋯ = ofBitVec n

theorem Int8.ofBitVec_ofNatLT (n : Nat) (hn : n < 2 ^ 8) : ofBitVec n#'hn = ofNat n

theorem Int16.ofBitVec_ofNatLT (n : Nat) (hn : n < 2 ^ 16) : ofBitVec n#'hn = ofNat n

theorem Int32.ofBitVec_ofNatLT (n : Nat) (hn : n < 2 ^ 32) : ofBitVec n#'hn = ofNat n

theorem Int64.ofBitVec_ofNatLT (n : Nat) (hn : n < 2 ^ 64) : ofBitVec n#'hn = ofNat n

theorem ISize.ofBitVec_ofNatLT (n : Nat) (hn : n < 2 ^ System.Platform.numBits) : ofBitVec n#'hn = ofNat n

@[simp]

theorem Int8.ofBitVec_ofNat (n : Nat) : ofBitVec (BitVec.ofNat 8 n) = ofNat n

@[simp]

theorem Int16.ofBitVec_ofNat (n : Nat) : ofBitVec (BitVec.ofNat 16 n) = ofNat n

@[simp]

theorem Int32.ofBitVec_ofNat (n : Nat) : ofBitVec (BitVec.ofNat 32 n) = ofNat n

@[simp]

theorem Int64.ofBitVec_ofNat (n : Nat) : ofBitVec (BitVec.ofNat 64 n) = ofNat n

@[simp]

theorem ISize.ofBitVec_ofNat (n : Nat) : ofBitVec (BitVec.ofNat System.Platform.numBits n) = ofNat n

@[simp]

theorem Int8.ofBitVec_ofInt (n : Int) : ofBitVec (BitVec.ofInt 8 n) = ofInt n

@[simp]

theorem Int16.ofBitVec_ofInt (n : Int) : ofBitVec (BitVec.ofInt 16 n) = ofInt n

@[simp]

theorem Int32.ofBitVec_ofInt (n : Int) : ofBitVec (BitVec.ofInt 32 n) = ofInt n

@[simp]

theorem Int64.ofBitVec_ofInt (n : Int) : ofBitVec (BitVec.ofInt 64 n) = ofInt n

@[simp]

theorem ISize.ofBitVec_ofInt (n : Int) : ofBitVec (BitVec.ofInt System.Platform.numBits n) = ofInt n

@[simp]

theorem Int8.ofNat_bitVecToNat (n : BitVec 8) : ofNat n.toNat = ofBitVec n

@[simp]

theorem Int16.ofNat_bitVecToNat (n : BitVec 16) : ofNat n.toNat = ofBitVec n

@[simp]

theorem Int32.ofNat_bitVecToNat (n : BitVec 32) : ofNat n.toNat = ofBitVec n

@[simp]

theorem Int64.ofNat_bitVecToNat (n : BitVec 64) : ofNat n.toNat = ofBitVec n

@[simp]

theorem ISize.ofNat_bitVecToNat (n : BitVec System.Platform.numBits) : ofNat n.toNat = ofBitVec n

@[simp]

theorem Int8.ofInt_bitVecToInt (n : BitVec 8) : ofInt n.toInt = ofBitVec n

@[simp]

theorem Int16.ofInt_bitVecToInt (n : BitVec 16) : ofInt n.toInt = ofBitVec n

@[simp]

theorem Int32.ofInt_bitVecToInt (n : BitVec 32) : ofInt n.toInt = ofBitVec n

@[simp]

theorem Int64.ofInt_bitVecToInt (n : BitVec 64) : ofInt n.toInt = ofBitVec n

@[simp]

theorem ISize.ofInt_bitVecToInt (n : BitVec System.Platform.numBits) : ofInt n.toInt = ofBitVec n

@[simp]

theorem Int8.ofIntClamp_bitVecToInt (n : BitVec 8) : ofIntClamp n.toInt = ofBitVec n

@[simp]

theorem Int16.ofIntClamp_bitVecToInt (n : BitVec 16) : ofIntClamp n.toInt = ofBitVec n

@[simp]

theorem Int32.ofIntClamp_bitVecToInt (n : BitVec 32) : ofIntClamp n.toInt = ofBitVec n

@[simp]

theorem Int64.ofIntClamp_bitVecToInt (n : BitVec 64) : ofIntClamp n.toInt = ofBitVec n

@[simp]

theorem ISize.ofIntClamp_bitVecToInt (n : BitVec System.Platform.numBits) : ofIntClamp n.toInt = ofBitVec n

@[deprecated Int8.ofIntLE_eq_ofIntClamp (since := "2026-05-04")]

theorem Int8.ofIntLE_eq_ofIntTruncate {x : Int} {h₁ : minValue.toInt ≤ x} {h₂ : x ≤ maxValue.toInt} : ofIntLE x h₁ h₂ = ofIntClamp x

@[deprecated Int16.ofIntLE_eq_ofIntClamp (since := "2026-05-04")]

theorem Int16.ofIntLE_eq_ofIntTruncate {x : Int} {h₁ : minValue.toInt ≤ x} {h₂ : x ≤ maxValue.toInt} : ofIntLE x h₁ h₂ = ofIntClamp x

@[deprecated Int32.ofIntLE_eq_ofIntClamp (since := "2026-05-04")]

theorem Int32.ofIntLE_eq_ofIntTruncate {x : Int} {h₁ : minValue.toInt ≤ x} {h₂ : x ≤ maxValue.toInt} : ofIntLE x h₁ h₂ = ofIntClamp x

@[deprecated Int64.ofIntLE_eq_ofIntClamp (since := "2026-05-04")]

theorem Int64.ofIntLE_eq_ofIntTruncate {x : Int} {h₁ : minValue.toInt ≤ x} {h₂ : x ≤ maxValue.toInt} : ofIntLE x h₁ h₂ = ofIntClamp x

@[deprecated ISize.ofIntLE_eq_ofIntClamp (since := "2026-05-04")]

theorem ISize.ofIntLE_eq_ofIntTruncate {x : Int} {h₁ : minValue.toInt ≤ x} {h₂ : x ≤ maxValue.toInt} : ofIntLE x h₁ h₂ = ofIntClamp x

@[deprecated Int8.toInt_ofIntClamp (since := "2026-05-04")]

theorem Int8.toInt_ofIntTruncate {x : Int} (h₁ : minValue.toInt ≤ x) (h₂ : x ≤ maxValue.toInt) : (ofIntClamp x).toInt = x

@[deprecated Int16.toInt_ofIntClamp (since := "2026-05-04")]

theorem Int16.toInt_ofIntTruncate {x : Int} (h₁ : minValue.toInt ≤ x) (h₂ : x ≤ maxValue.toInt) : (ofIntClamp x).toInt = x

@[deprecated Int32.toInt_ofIntClamp (since := "2026-05-04")]

theorem Int32.toInt_ofIntTruncate {x : Int} (h₁ : minValue.toInt ≤ x) (h₂ : x ≤ maxValue.toInt) : (ofIntClamp x).toInt = x

@[deprecated Int64.toInt_ofIntClamp (since := "2026-05-04")]

theorem Int64.toInt_ofIntTruncate {x : Int} (h₁ : minValue.toInt ≤ x) (h₂ : x ≤ maxValue.toInt) : (ofIntClamp x).toInt = x

@[deprecated ISize.toInt_ofIntClamp (since := "2026-05-04")]

theorem ISize.toInt_ofIntTruncate {x : Int} (h₁ : minValue.toInt ≤ x) (h₂ : x ≤ maxValue.toInt) : (ofIntClamp x).toInt = x

@[deprecated Int8.ofIntClamp_toInt (since := "2026-05-04")]

theorem Int8.ofIntTruncate_toInt (x : Int8) : ofIntClamp x.toInt = x

@[deprecated Int16.ofIntClamp_toInt (since := "2026-05-04")]

theorem Int16.ofIntTruncate_toInt (x : Int16) : ofIntClamp x.toInt = x

@[deprecated Int32.ofIntClamp_toInt (since := "2026-05-04")]

theorem Int32.ofIntTruncate_toInt (x : Int32) : ofIntClamp x.toInt = x

@[deprecated Int64.ofIntClamp_toInt (since := "2026-05-04")]

theorem Int64.ofIntTruncate_toInt (x : Int64) : ofIntClamp x.toInt = x

@[deprecated ISize.ofIntClamp_toInt (since := "2026-05-04")]

theorem ISize.ofIntTruncate_toInt (x : ISize) : ofIntClamp x.toInt = x

@[deprecated Int16.ofIntClamp_int8ToInt (since := "2026-05-04")]

theorem Int16.ofIntTruncate_int8ToInt (x : Int8) : ofIntClamp x.toInt = x.toInt16

@[deprecated Int32.ofIntClamp_int8ToInt (since := "2026-05-04")]

theorem Int32.ofIntTruncate_int8ToInt (x : Int8) : ofIntClamp x.toInt = x.toInt32

@[deprecated Int64.ofIntClamp_int8ToInt (since := "2026-05-04")]

theorem Int64.ofIntTruncate_int8ToInt (x : Int8) : ofIntClamp x.toInt = x.toInt64

@[deprecated ISize.ofIntClamp_int8ToInt (since := "2026-05-04")]

theorem ISize.ofIntTruncate_int8ToInt (x : Int8) : ofIntClamp x.toInt = x.toISize

@[deprecated Int32.ofIntClamp_int16ToInt (since := "2026-05-04")]

theorem Int32.ofIntTruncate_int16ToInt (x : Int16) : ofIntClamp x.toInt = x.toInt32

@[deprecated Int64.ofIntClamp_int16ToInt (since := "2026-05-04")]

theorem Int64.ofIntTruncate_int16ToInt (x : Int16) : ofIntClamp x.toInt = x.toInt64

@[deprecated ISize.ofIntClamp_int16ToInt (since := "2026-05-04")]

theorem ISize.ofIntTruncate_int16ToInt (x : Int16) : ofIntClamp x.toInt = x.toISize

@[deprecated Int64.ofIntClamp_int32ToInt (since := "2026-05-04")]

theorem Int64.ofIntTruncate_int32ToInt (x : Int32) : ofIntClamp x.toInt = x.toInt64

@[deprecated ISize.ofIntClamp_int32ToInt (since := "2026-05-04")]

theorem ISize.ofIntTruncate_int32ToInt (x : Int32) : ofIntClamp x.toInt = x.toISize

@[deprecated Int64.ofIntClamp_iSizeToInt (since := "2026-05-04")]

theorem Int64.ofIntTruncate_iSizeToInt (x : ISize) : ofIntClamp x.toInt = x.toInt64

@[deprecated Int8.toBitVec_ofIntClamp (since := "2026-05-04")]

theorem Int8.toBitVec_ofIntTruncate {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntClamp n).toBitVec = BitVec.ofInt 8 n

@[deprecated Int16.toBitVec_ofIntClamp (since := "2026-05-04")]

theorem Int16.toBitVec_ofIntTruncate {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntClamp n).toBitVec = BitVec.ofInt 16 n

@[deprecated Int32.toBitVec_ofIntClamp (since := "2026-05-04")]

theorem Int32.toBitVec_ofIntTruncate {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntClamp n).toBitVec = BitVec.ofInt 32 n

@[deprecated Int64.toBitVec_ofIntClamp (since := "2026-05-04")]

theorem Int64.toBitVec_ofIntTruncate {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntClamp n).toBitVec = BitVec.ofInt 64 n

@[deprecated ISize.toBitVec_ofIntClamp (since := "2026-05-04")]

theorem ISize.toBitVec_ofIntTruncate {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) : (ofIntClamp n).toBitVec = BitVec.ofInt System.Platform.numBits n

@[deprecated Int8.toNatClampNeg_ofIntClamp_of_lt (since := "2026-05-04")]

theorem Int8.toNatClampNeg_ofIntTruncate_of_lt {n : Int} (h₁ : n < 2 ^ 7) : (ofIntClamp n).toNatClampNeg = n.toNat

@[deprecated Int16.toNatClampNeg_ofIntClamp_of_lt (since := "2026-05-04")]

theorem Int16.toNatClampNeg_ofIntTruncate_of_lt {n : Int} (h₁ : n < 2 ^ 15) : (ofIntClamp n).toNatClampNeg = n.toNat

@[deprecated Int32.toNatClampNeg_ofIntClamp_of_lt (since := "2026-05-04")]

theorem Int32.toNatClampNeg_ofIntTruncate_of_lt {n : Int} (h₁ : n < 2 ^ 31) : (ofIntClamp n).toNatClampNeg = n.toNat

@[deprecated Int64.toNatClampNeg_ofIntClamp_of_lt (since := "2026-05-04")]

theorem Int64.toNatClampNeg_ofIntTruncate_of_lt {n : Int} (h₁ : n < 2 ^ 63) : (ofIntClamp n).toNatClampNeg = n.toNat

@[deprecated ISize.toNatClampNeg_ofIntClamp_of_lt_two_pow_numBits (since := "2026-05-04")]

theorem ISize.toNatClampNeg_ofIntTruncate_of_lt_two_pow_numBits {n : Int} (h₁ : n < 2 ^ (System.Platform.numBits - 1)) : (ofIntClamp n).toNatClampNeg = n.toNat

@[deprecated ISize.toNatClampNeg_ofIntClamp_of_lt (since := "2026-05-04")]

theorem ISize.toNatClampNeg_ofIntTruncate_of_lt {n : Int} (h₁ : n < 2 ^ 31) : (ofIntClamp n).toNatClampNeg = n.toNat

@[deprecated Int16.toInt8_ofIntClamp (since := "2026-05-04")]

theorem Int16.toInt8_ofIntTruncate {n : Int} (h₁ : -2 ^ 15 ≤ n) (h₂ : n < 2 ^ 15) : (ofIntClamp n).toInt8 = Int8.ofInt n

@[deprecated Int32.toInt8_ofIntClamp (since := "2026-05-04")]

theorem Int32.toInt8_ofIntTruncate {n : Int} (h₁ : -2 ^ 31 ≤ n) (h₂ : n < 2 ^ 31) : (ofIntClamp n).toInt8 = Int8.ofInt n

@[deprecated Int64.toInt8_ofIntClamp (since := "2026-05-04")]

theorem Int64.toInt8_ofIntTruncate {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) : (ofIntClamp n).toInt8 = Int8.ofInt n

@[deprecated ISize.toInt8_ofIntClamp (since := "2026-05-04")]

theorem ISize.toInt8_ofIntTruncate {n : Int} (h₁ : -2 ^ (System.Platform.numBits - 1) ≤ n) (h₂ : n < 2 ^ (System.Platform.numBits - 1)) : (ofIntClamp n).toInt8 = Int8.ofInt n

@[deprecated Int32.toInt16_ofIntClamp (since := "2026-05-04")]

theorem Int32.toInt16_ofIntTruncate {n : Int} (h₁ : -2 ^ 31 ≤ n) (h₂ : n < 2 ^ 31) : (ofIntClamp n).toInt16 = Int16.ofInt n

@[deprecated Int64.toInt16_ofIntClamp (since := "2026-05-04")]

theorem Int64.toInt16_ofIntTruncate {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) : (ofIntClamp n).toInt16 = Int16.ofInt n

@[deprecated ISize.toInt16_ofIntClamp (since := "2026-05-04")]

theorem ISize.toInt16_ofIntTruncate {n : Int} (h₁ : -2 ^ (System.Platform.numBits - 1) ≤ n) (h₂ : n < 2 ^ (System.Platform.numBits - 1)) : (ofIntClamp n).toInt16 = Int16.ofInt n

@[deprecated Int64.toInt32_ofIntClamp (since := "2026-05-04")]

theorem Int64.toInt32_ofIntTruncate {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) : (ofIntClamp n).toInt32 = Int32.ofInt n

@[deprecated ISize.toInt32_ofIntClamp (since := "2026-05-04")]

theorem ISize.toInt32_ofIntTruncate {n : Int} (h₁ : -2 ^ (System.Platform.numBits - 1) ≤ n) (h₂ : n < 2 ^ (System.Platform.numBits - 1)) : (ofIntClamp n).toInt32 = Int32.ofInt n

@[deprecated Int64.toISize_ofIntClamp (since := "2026-05-04")]

theorem Int64.toISize_ofIntTruncate {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) : (ofIntClamp n).toISize = ISize.ofInt n

@[deprecated Int8.ofIntClamp_bitVecToInt (since := "2026-05-04")]

theorem Int8.ofIntTruncate_bitVecToInt (n : BitVec 8) : ofIntClamp n.toInt = ofBitVec n

@[deprecated Int16.ofIntClamp_bitVecToInt (since := "2026-05-04")]

theorem Int16.ofIntTruncate_bitVecToInt (n : BitVec 16) : ofIntClamp n.toInt = ofBitVec n

@[deprecated Int32.ofIntClamp_bitVecToInt (since := "2026-05-04")]

theorem Int32.ofIntTruncate_bitVecToInt (n : BitVec 32) : ofIntClamp n.toInt = ofBitVec n

@[deprecated Int64.ofIntClamp_bitVecToInt (since := "2026-05-04")]

theorem Int64.ofIntTruncate_bitVecToInt (n : BitVec 64) : ofIntClamp n.toInt = ofBitVec n

@[deprecated ISize.ofIntClamp_bitVecToInt (since := "2026-05-04")]

theorem ISize.ofIntTruncate_bitVecToInt (n : BitVec System.Platform.numBits) : ofIntClamp n.toInt = ofBitVec n

@[simp]

theorem Int8.toInt_neg (n : Int8) : (-n).toInt = (-n.toInt).bmod (2 ^ 8)

@[simp]

theorem Int16.toInt_neg (n : Int16) : (-n).toInt = (-n.toInt).bmod (2 ^ 16)

@[simp]

theorem Int32.toInt_neg (n : Int32) : (-n).toInt = (-n.toInt).bmod (2 ^ 32)

@[simp]

theorem Int64.toInt_neg (n : Int64) : (-n).toInt = (-n.toInt).bmod (2 ^ 64)

theorem ISize.toInt_neg (n : ISize) : (-n).toInt = (-n.toInt).bmod (2 ^ System.Platform.numBits)

@[simp]

theorem Int8.toNatClampNeg_eq_zero_iff {n : Int8} : n.toNatClampNeg = 0 ↔ n ≤ 0

@[simp]

theorem Int16.toNatClampNeg_eq_zero_iff {n : Int16} : n.toNatClampNeg = 0 ↔ n ≤ 0

@[simp]

theorem Int32.toNatClampNeg_eq_zero_iff {n : Int32} : n.toNatClampNeg = 0 ↔ n ≤ 0

@[simp]

theorem Int64.toNatClampNeg_eq_zero_iff {n : Int64} : n.toNatClampNeg = 0 ↔ n ≤ 0

@[simp]

theorem ISize.toNatClampNeg_eq_zero_iff {n : ISize} : n.toNatClampNeg = 0 ↔ n ≤ 0

@[simp]

theorem Int8.not_le {n m : Int8} : ¬n ≤ m ↔ m < n

@[simp]

theorem Int16.not_le {n m : Int16} : ¬n ≤ m ↔ m < n

@[simp]

theorem Int32.not_le {n m : Int32} : ¬n ≤ m ↔ m < n

@[simp]

theorem Int64.not_le {n m : Int64} : ¬n ≤ m ↔ m < n

@[simp]

theorem ISize.not_le {n m : ISize} : ¬n ≤ m ↔ m < n

@[simp]

theorem Int8.neg_nonpos_iff (n : Int8) : -n ≤ 0 ↔ n = minValue ∨ 0 ≤ n

@[simp]

theorem Int16.neg_nonpos_iff (n : Int16) : -n ≤ 0 ↔ n = minValue ∨ 0 ≤ n

@[simp]

theorem Int32.neg_nonpos_iff (n : Int32) : -n ≤ 0 ↔ n = minValue ∨ 0 ≤ n

@[simp]

theorem Int64.neg_nonpos_iff (n : Int64) : -n ≤ 0 ↔ n = minValue ∨ 0 ≤ n

@[simp]

theorem ISize.neg_nonpos_iff (n : ISize) : -n ≤ 0 ↔ n = minValue ∨ 0 ≤ n

@[simp]

theorem Int8.toNatClampNeg_pos_iff (n : Int8) : 0 < n.toNatClampNeg ↔ 0 < n

@[simp]

theorem Int16.toNatClampNeg_pos_iff (n : Int16) : 0 < n.toNatClampNeg ↔ 0 < n

@[simp]

theorem Int32.toNatClampNeg_pos_iff (n : Int32) : 0 < n.toNatClampNeg ↔ 0 < n

@[simp]

theorem Int64.toNatClampNeg_pos_iff (n : Int64) : 0 < n.toNatClampNeg ↔ 0 < n

@[simp]

theorem ISize.toNatClampNeg_pos_iff (n : ISize) : 0 < n.toNatClampNeg ↔ 0 < n

@[simp]

theorem Int8.toInt_div (a b : Int8) : (a / b).toInt = (a.toInt.tdiv b.toInt).bmod (2 ^ 8)

@[simp]

theorem Int16.toInt_div (a b : Int16) : (a / b).toInt = (a.toInt.tdiv b.toInt).bmod (2 ^ 16)

@[simp]

theorem Int32.toInt_div (a b : Int32) : (a / b).toInt = (a.toInt.tdiv b.toInt).bmod (2 ^ 32)

@[simp]

theorem Int64.toInt_div (a b : Int64) : (a / b).toInt = (a.toInt.tdiv b.toInt).bmod (2 ^ 64)

@[simp]

theorem ISize.toInt_div (a b : ISize) : (a / b).toInt = (a.toInt.tdiv b.toInt).bmod (2 ^ System.Platform.numBits)

theorem Int8.toInt_div_of_ne_left (a b : Int8) (h : a ≠ minValue) : (a / b).toInt = a.toInt.tdiv b.toInt

theorem Int16.toInt_div_of_ne_left (a b : Int16) (h : a ≠ minValue) : (a / b).toInt = a.toInt.tdiv b.toInt

theorem Int32.toInt_div_of_ne_left (a b : Int32) (h : a ≠ minValue) : (a / b).toInt = a.toInt.tdiv b.toInt

theorem Int64.toInt_div_of_ne_left (a b : Int64) (h : a ≠ minValue) : (a / b).toInt = a.toInt.tdiv b.toInt

theorem ISize.toInt_div_of_ne_left (a b : ISize) (h : a ≠ minValue) : (a / b).toInt = a.toInt.tdiv b.toInt

theorem Int8.toInt_div_of_ne_right (a b : Int8) (h : b ≠ -1) : (a / b).toInt = a.toInt.tdiv b.toInt

theorem Int16.toInt_div_of_ne_right (a b : Int16) (h : b ≠ -1) : (a / b).toInt = a.toInt.tdiv b.toInt

theorem Int32.toInt_div_of_ne_right (a b : Int32) (h : b ≠ -1) : (a / b).toInt = a.toInt.tdiv b.toInt

theorem Int64.toInt_div_of_ne_right (a b : Int64) (h : b ≠ -1) : (a / b).toInt = a.toInt.tdiv b.toInt

theorem ISize.toInt_div_of_ne_right (a b : ISize) (h : b ≠ -1) : (a / b).toInt = a.toInt.tdiv b.toInt

theorem Int8.toInt16_ne_minValue (a : Int8) : a.toInt16 ≠ Int16.minValue

theorem Int8.toInt32_ne_minValue (a : Int8) : a.toInt32 ≠ Int32.minValue

theorem Int8.toInt64_ne_minValue (a : Int8) : a.toInt64 ≠ Int64.minValue

theorem Int8.toISize_ne_minValue (a : Int8) : a.toISize ≠ ISize.minValue

theorem Int16.toInt32_ne_minValue (a : Int16) : a.toInt32 ≠ Int32.minValue

theorem Int16.toInt64_ne_minValue (a : Int16) : a.toInt64 ≠ Int64.minValue

theorem Int16.toISize_ne_minValue (a : Int16) : a.toISize ≠ ISize.minValue

theorem Int32.toInt64_ne_minValue (a : Int32) : a.toInt64 ≠ Int64.minValue

theorem Int32.toISize_ne_minValue (a : Int32) (ha : a ≠ minValue) : a.toISize ≠ ISize.minValue

theorem ISize.toInt64_ne_minValue (a : ISize) (ha : a ≠ minValue) : a.toInt64 ≠ Int64.minValue

theorem Int8.toInt16_ne_neg_one (a : Int8) (ha : a ≠ -1) : a.toInt16 ≠ -1

theorem Int8.toInt32_ne_neg_one (a : Int8) (ha : a ≠ -1) : a.toInt32 ≠ -1

theorem Int8.toInt64_ne_neg_one (a : Int8) (ha : a ≠ -1) : a.toInt64 ≠ -1

theorem Int8.toISize_ne_neg_one (a : Int8) (ha : a ≠ -1) : a.toISize ≠ -1

theorem Int16.toInt32_ne_neg_one (a : Int16) (ha : a ≠ -1) : a.toInt32 ≠ -1

theorem Int16.toInt64_ne_neg_one (a : Int16) (ha : a ≠ -1) : a.toInt64 ≠ -1

theorem Int16.toISize_ne_neg_one (a : Int16) (ha : a ≠ -1) : a.toISize ≠ -1

theorem Int32.toInt64_ne_neg_one (a : Int32) (ha : a ≠ -1) : a.toInt64 ≠ -1

theorem Int32.toISize_ne_neg_one (a : Int32) (ha : a ≠ -1) : a.toISize ≠ -1

theorem ISize.toInt64_ne_neg_one (a : ISize) (ha : a ≠ -1) : a.toInt64 ≠ -1

theorem Int8.toInt16_div_of_ne_left (a b : Int8) (ha : a ≠ minValue) : (a / b).toInt16 = a.toInt16 / b.toInt16

theorem Int8.toInt32_div_of_ne_left (a b : Int8) (ha : a ≠ minValue) : (a / b).toInt32 = a.toInt32 / b.toInt32

theorem Int8.toInt64_div_of_ne_left (a b : Int8) (ha : a ≠ minValue) : (a / b).toInt64 = a.toInt64 / b.toInt64

theorem Int8.toISize_div_of_ne_left (a b : Int8) (ha : a ≠ minValue) : (a / b).toISize = a.toISize / b.toISize

theorem Int16.toInt32_div_of_ne_left (a b : Int16) (ha : a ≠ minValue) : (a / b).toInt32 = a.toInt32 / b.toInt32

theorem Int16.toInt64_div_of_ne_left (a b : Int16) (ha : a ≠ minValue) : (a / b).toInt64 = a.toInt64 / b.toInt64

theorem Int16.toISize_div_of_ne_left (a b : Int16) (ha : a ≠ minValue) : (a / b).toISize = a.toISize / b.toISize

theorem Int32.toInt64_div_of_ne_left (a b : Int32) (ha : a ≠ minValue) : (a / b).toInt64 = a.toInt64 / b.toInt64

theorem Int32.toISize_div_of_ne_left (a b : Int32) (ha : a ≠ minValue) : (a / b).toISize = a.toISize / b.toISize

theorem ISize.toInt64_div_of_ne_left (a b : ISize) (ha : a ≠ minValue) : (a / b).toInt64 = a.toInt64 / b.toInt64

theorem Int8.toInt16_div_of_ne_right (a b : Int8) (hb : b ≠ -1) : (a / b).toInt16 = a.toInt16 / b.toInt16

theorem Int8.toInt32_div_of_ne_right (a b : Int8) (hb : b ≠ -1) : (a / b).toInt32 = a.toInt32 / b.toInt32

theorem Int8.toInt64_div_of_ne_right (a b : Int8) (hb : b ≠ -1) : (a / b).toInt64 = a.toInt64 / b.toInt64

theorem Int8.toISize_div_of_ne_right (a b : Int8) (hb : b ≠ -1) : (a / b).toISize = a.toISize / b.toISize

theorem Int16.toInt32_div_of_ne_right (a b : Int16) (hb : b ≠ -1) : (a / b).toInt32 = a.toInt32 / b.toInt32

theorem Int16.toInt64_div_of_ne_right (a b : Int16) (hb : b ≠ -1) : (a / b).toInt64 = a.toInt64 / b.toInt64

theorem Int16.toISize_div_of_ne_right (a b : Int16) (hb : b ≠ -1) : (a / b).toISize = a.toISize / b.toISize

theorem Int32.toInt64_div_of_ne_right (a b : Int32) (hb : b ≠ -1) : (a / b).toInt64 = a.toInt64 / b.toInt64

theorem Int32.toISize_div_of_ne_right (a b : Int32) (hb : b ≠ -1) : (a / b).toISize = a.toISize / b.toISize

theorem ISize.toInt64_div_of_ne_right (a b : ISize) (hb : b ≠ -1) : (a / b).toInt64 = a.toInt64 / b.toInt64

@[simp]

theorem Int8.minValue_div_neg_one : minValue / -1 = minValue

@[simp]

theorem Int16.minValue_div_neg_one : minValue / -1 = minValue

@[simp]

theorem Int32.minValue_div_neg_one : minValue / -1 = minValue

@[simp]

theorem Int64.minValue_div_neg_one : minValue / -1 = minValue

@[simp]

theorem ISize.minValue_div_neg_one : minValue / -1 = minValue

@[simp]

theorem Int8.toInt_add (a b : Int8) : (a + b).toInt = (a.toInt + b.toInt).bmod (2 ^ 8)

@[simp]

theorem Int16.toInt_add (a b : Int16) : (a + b).toInt = (a.toInt + b.toInt).bmod (2 ^ 16)

@[simp]

theorem Int32.toInt_add (a b : Int32) : (a + b).toInt = (a.toInt + b.toInt).bmod (2 ^ 32)

@[simp]

theorem Int64.toInt_add (a b : Int64) : (a + b).toInt = (a.toInt + b.toInt).bmod (2 ^ 64)

@[simp]

theorem ISize.toInt_add (a b : ISize) : (a + b).toInt = (a.toInt + b.toInt).bmod (2 ^ System.Platform.numBits)

@[simp]

theorem Int16.toInt8_add (a b : Int16) : (a + b).toInt8 = a.toInt8 + b.toInt8

@[simp]

theorem Int32.toInt8_add (a b : Int32) : (a + b).toInt8 = a.toInt8 + b.toInt8

@[simp]

theorem Int32.toInt16_add (a b : Int32) : (a + b).toInt16 = a.toInt16 + b.toInt16

@[simp]

theorem ISize.toInt8_add (a b : ISize) : (a + b).toInt8 = a.toInt8 + b.toInt8

@[simp]

theorem ISize.toInt16_add (a b : ISize) : (a + b).toInt16 = a.toInt16 + b.toInt16

@[simp]

theorem ISize.toInt32_add (a b : ISize) : (a + b).toInt32 = a.toInt32 + b.toInt32

@[simp]

theorem Int64.toInt8_add (a b : Int64) : (a + b).toInt8 = a.toInt8 + b.toInt8

@[simp]

theorem Int64.toInt16_add (a b : Int64) : (a + b).toInt16 = a.toInt16 + b.toInt16

@[simp]

theorem Int64.toInt32_add (a b : Int64) : (a + b).toInt32 = a.toInt32 + b.toInt32

@[simp]

theorem Int64.toISize_add (a b : Int64) : (a + b).toISize = a.toISize + b.toISize

@[simp]

theorem Int8.toInt_mul (a b : Int8) : (a * b).toInt = (a.toInt * b.toInt).bmod (2 ^ 8)

@[simp]

theorem Int16.toInt_mul (a b : Int16) : (a * b).toInt = (a.toInt * b.toInt).bmod (2 ^ 16)

@[simp]

theorem Int32.toInt_mul (a b : Int32) : (a * b).toInt = (a.toInt * b.toInt).bmod (2 ^ 32)

@[simp]

theorem Int64.toInt_mul (a b : Int64) : (a * b).toInt = (a.toInt * b.toInt).bmod (2 ^ 64)

@[simp]

theorem ISize.toInt_mul (a b : ISize) : (a * b).toInt = (a.toInt * b.toInt).bmod (2 ^ System.Platform.numBits)

@[simp]

theorem Int16.toInt8_mul (a b : Int16) : (a * b).toInt8 = a.toInt8 * b.toInt8

@[simp]

theorem Int32.toInt8_mul (a b : Int32) : (a * b).toInt8 = a.toInt8 * b.toInt8

@[simp]

theorem Int32.toInt16_mul (a b : Int32) : (a * b).toInt16 = a.toInt16 * b.toInt16

@[simp]

theorem ISize.toInt8_mul (a b : ISize) : (a * b).toInt8 = a.toInt8 * b.toInt8

@[simp]

theorem ISize.toInt16_mul (a b : ISize) : (a * b).toInt16 = a.toInt16 * b.toInt16

@[simp]

theorem ISize.toInt32_mul (a b : ISize) : (a * b).toInt32 = a.toInt32 * b.toInt32

@[simp]

theorem Int64.toInt8_mul (a b : Int64) : (a * b).toInt8 = a.toInt8 * b.toInt8

@[simp]

theorem Int64.toInt16_mul (a b : Int64) : (a * b).toInt16 = a.toInt16 * b.toInt16

@[simp]

theorem Int64.toInt32_mul (a b : Int64) : (a * b).toInt32 = a.toInt32 * b.toInt32

@[simp]

theorem Int64.toISize_mul (a b : Int64) : (a * b).toISize = a.toISize * b.toISize

theorem Int8.sub_eq_add_neg (a b : Int8) : a - b = a + -b

theorem Int16.sub_eq_add_neg (a b : Int16) : a - b = a + -b

theorem Int32.sub_eq_add_neg (a b : Int32) : a - b = a + -b

theorem Int64.sub_eq_add_neg (a b : Int64) : a - b = a + -b

theorem ISize.sub_eq_add_neg (a b : ISize) : a - b = a + -b

@[simp]

theorem Int8.toInt_sub (a b : Int8) : (a - b).toInt = (a.toInt - b.toInt).bmod (2 ^ 8)

@[simp]

theorem Int16.toInt_sub (a b : Int16) : (a - b).toInt = (a.toInt - b.toInt).bmod (2 ^ 16)

@[simp]

theorem Int32.toInt_sub (a b : Int32) : (a - b).toInt = (a.toInt - b.toInt).bmod (2 ^ 32)

@[simp]

theorem Int64.toInt_sub (a b : Int64) : (a - b).toInt = (a.toInt - b.toInt).bmod (2 ^ 64)

@[simp]

theorem ISize.toInt_sub (a b : ISize) : (a - b).toInt = (a.toInt - b.toInt).bmod (2 ^ System.Platform.numBits)

@[simp]

theorem Int16.toInt8_sub (a b : Int16) : (a - b).toInt8 = a.toInt8 - b.toInt8

@[simp]

theorem Int32.toInt8_sub (a b : Int32) : (a - b).toInt8 = a.toInt8 - b.toInt8

@[simp]

theorem Int32.toInt16_sub (a b : Int32) : (a - b).toInt16 = a.toInt16 - b.toInt16

@[simp]

theorem ISize.toInt8_sub (a b : ISize) : (a - b).toInt8 = a.toInt8 - b.toInt8

@[simp]

theorem ISize.toInt16_sub (a b : ISize) : (a - b).toInt16 = a.toInt16 - b.toInt16

@[simp]

theorem ISize.toInt32_sub (a b : ISize) : (a - b).toInt32 = a.toInt32 - b.toInt32

@[simp]

theorem Int64.toInt8_sub (a b : Int64) : (a - b).toInt8 = a.toInt8 - b.toInt8

@[simp]

theorem Int64.toInt16_sub (a b : Int64) : (a - b).toInt16 = a.toInt16 - b.toInt16

@[simp]

theorem Int64.toInt32_sub (a b : Int64) : (a - b).toInt32 = a.toInt32 - b.toInt32

@[simp]

theorem Int64.toISize_sub (a b : Int64) : (a - b).toISize = a.toISize - b.toISize

@[simp]

theorem Int8.toInt16_lt {a b : Int8} : a.toInt16 < b.toInt16 ↔ a < b

@[simp]

theorem Int8.toInt32_lt {a b : Int8} : a.toInt32 < b.toInt32 ↔ a < b

@[simp]

theorem Int8.toInt64_lt {a b : Int8} : a.toInt64 < b.toInt64 ↔ a < b

@[simp]

theorem Int8.toISize_lt {a b : Int8} : a.toISize < b.toISize ↔ a < b

@[simp]

theorem Int16.toInt32_lt {a b : Int16} : a.toInt32 < b.toInt32 ↔ a < b

@[simp]

theorem Int16.toInt64_lt {a b : Int16} : a.toInt64 < b.toInt64 ↔ a < b

@[simp]

theorem Int16.toISize_lt {a b : Int16} : a.toISize < b.toISize ↔ a < b

@[simp]

theorem Int32.toInt64_lt {a b : Int32} : a.toInt64 < b.toInt64 ↔ a < b

@[simp]

theorem Int32.toISize_lt {a b : Int32} : a.toISize < b.toISize ↔ a < b

@[simp]

theorem ISize.toInt64_lt {a b : ISize} : a.toInt64 < b.toInt64 ↔ a < b

@[simp]

theorem Int8.toInt16_le {a b : Int8} : a.toInt16 ≤ b.toInt16 ↔ a ≤ b

@[simp]

theorem Int8.toInt32_le {a b : Int8} : a.toInt32 ≤ b.toInt32 ↔ a ≤ b

@[simp]

theorem Int8.toInt64_le {a b : Int8} : a.toInt64 ≤ b.toInt64 ↔ a ≤ b

@[simp]

theorem Int8.toISize_le {a b : Int8} : a.toISize ≤ b.toISize ↔ a ≤ b

@[simp]

theorem Int16.toInt32_le {a b : Int16} : a.toInt32 ≤ b.toInt32 ↔ a ≤ b

@[simp]

theorem Int16.toInt64_le {a b : Int16} : a.toInt64 ≤ b.toInt64 ↔ a ≤ b

@[simp]

theorem Int16.toISize_le {a b : Int16} : a.toISize ≤ b.toISize ↔ a ≤ b

@[simp]

theorem Int32.toInt64_le {a b : Int32} : a.toInt64 ≤ b.toInt64 ↔ a ≤ b

@[simp]

theorem Int32.toISize_le {a b : Int32} : a.toISize ≤ b.toISize ↔ a ≤ b

@[simp]

theorem ISize.toInt64_le {a b : ISize} : a.toInt64 ≤ b.toInt64 ↔ a ≤ b

@[simp]

theorem Int8.ofBitVec_neg (a : BitVec 8) : ofBitVec (-a) = -ofBitVec a

@[simp]

theorem Int16.ofBitVec_neg (a : BitVec 16) : ofBitVec (-a) = -ofBitVec a

@[simp]

theorem Int32.ofBitVec_neg (a : BitVec 32) : ofBitVec (-a) = -ofBitVec a

@[simp]

theorem Int64.ofBitVec_neg (a : BitVec 64) : ofBitVec (-a) = -ofBitVec a

@[simp]

theorem ISize.ofBitVec_neg (a : BitVec System.Platform.numBits) : ofBitVec (-a) = -ofBitVec a

@[simp]

theorem Int8.ofInt_neg (a : Int) : ofInt (-a) = -ofInt a

@[simp]

theorem Int16.ofInt_neg (a : Int) : ofInt (-a) = -ofInt a

@[simp]

theorem Int32.ofInt_neg (a : Int) : ofInt (-a) = -ofInt a

@[simp]

theorem Int64.ofInt_neg (a : Int) : ofInt (-a) = -ofInt a

@[simp]

theorem ISize.ofInt_neg (a : Int) : ofInt (-a) = -ofInt a

theorem Int8.ofInt_eq_iff_bmod_eq_toInt (a : Int) (b : Int8) : ofInt a = b ↔ a.bmod (2 ^ 8) = b.toInt

theorem Int16.ofInt_eq_iff_bmod_eq_toInt (a : Int) (b : Int16) : ofInt a = b ↔ a.bmod (2 ^ 16) = b.toInt

theorem Int32.ofInt_eq_iff_bmod_eq_toInt (a : Int) (b : Int32) : ofInt a = b ↔ a.bmod (2 ^ 32) = b.toInt

theorem Int64.ofInt_eq_iff_bmod_eq_toInt (a : Int) (b : Int64) : ofInt a = b ↔ a.bmod (2 ^ 64) = b.toInt

theorem ISize.ofInt_eq_iff_bmod_eq_toInt (a : Int) (b : ISize) : ofInt a = b ↔ a.bmod (2 ^ System.Platform.numBits) = b.toInt

@[simp]

theorem Int8.ofBitVec_add (a b : BitVec 8) : ofBitVec (a + b) = ofBitVec a + ofBitVec b

@[simp]

theorem Int16.ofBitVec_add (a b : BitVec 16) : ofBitVec (a + b) = ofBitVec a + ofBitVec b

@[simp]

theorem Int32.ofBitVec_add (a b : BitVec 32) : ofBitVec (a + b) = ofBitVec a + ofBitVec b

@[simp]

theorem Int64.ofBitVec_add (a b : BitVec 64) : ofBitVec (a + b) = ofBitVec a + ofBitVec b

@[simp]

theorem ISize.ofBitVec_add (a b : BitVec System.Platform.numBits) : ofBitVec (a + b) = ofBitVec a + ofBitVec b

@[simp]

theorem Int8.ofInt_add (a b : Int) : ofInt (a + b) = ofInt a + ofInt b

@[simp]

theorem Int16.ofInt_add (a b : Int) : ofInt (a + b) = ofInt a + ofInt b

@[simp]

theorem Int32.ofInt_add (a b : Int) : ofInt (a + b) = ofInt a + ofInt b

@[simp]

theorem Int64.ofInt_add (a b : Int) : ofInt (a + b) = ofInt a + ofInt b

@[simp]

theorem ISize.ofInt_add (a b : Int) : ofInt (a + b) = ofInt a + ofInt b

@[simp]

theorem Int8.ofNat_add (a b : Nat) : ofNat (a + b) = ofNat a + ofNat b

@[simp]

theorem Int16.ofNat_add (a b : Nat) : ofNat (a + b) = ofNat a + ofNat b

@[simp]

theorem Int32.ofNat_add (a b : Nat) : ofNat (a + b) = ofNat a + ofNat b

@[simp]

theorem Int64.ofNat_add (a b : Nat) : ofNat (a + b) = ofNat a + ofNat b

@[simp]

theorem ISize.ofNat_add (a b : Nat) : ofNat (a + b) = ofNat a + ofNat b

theorem Int8.ofIntLE_add {a b : Int} {hab₁ : minValue.toInt ≤ a + b} {hab₂ : a + b ≤ maxValue.toInt} : ofIntLE (a + b) hab₁ hab₂ = ofInt a + ofInt b

theorem Int16.ofIntLE_add {a b : Int} {hab₁ : minValue.toInt ≤ a + b} {hab₂ : a + b ≤ maxValue.toInt} : ofIntLE (a + b) hab₁ hab₂ = ofInt a + ofInt b

theorem Int32.ofIntLE_add {a b : Int} {hab₁ : minValue.toInt ≤ a + b} {hab₂ : a + b ≤ maxValue.toInt} : ofIntLE (a + b) hab₁ hab₂ = ofInt a + ofInt b

theorem Int64.ofIntLE_add {a b : Int} {hab₁ : minValue.toInt ≤ a + b} {hab₂ : a + b ≤ maxValue.toInt} : ofIntLE (a + b) hab₁ hab₂ = ofInt a + ofInt b

theorem ISize.ofIntLE_add {a b : Int} {hab₁ : minValue.toInt ≤ a + b} {hab₂ : a + b ≤ maxValue.toInt} : ofIntLE (a + b) hab₁ hab₂ = ofInt a + ofInt b

@[simp]

theorem Int8.ofBitVec_sub (a b : BitVec 8) : ofBitVec (a - b) = ofBitVec a - ofBitVec b

@[simp]

theorem Int16.ofBitVec_sub (a b : BitVec 16) : ofBitVec (a - b) = ofBitVec a - ofBitVec b

@[simp]

theorem Int32.ofBitVec_sub (a b : BitVec 32) : ofBitVec (a - b) = ofBitVec a - ofBitVec b

@[simp]

theorem Int64.ofBitVec_sub (a b : BitVec 64) : ofBitVec (a - b) = ofBitVec a - ofBitVec b

@[simp]

theorem ISize.ofBitVec_sub (a b : BitVec System.Platform.numBits) : ofBitVec (a - b) = ofBitVec a - ofBitVec b

@[simp]

theorem Int8.ofInt_sub (a b : Int) : ofInt (a - b) = ofInt a - ofInt b

@[simp]

theorem Int16.ofInt_sub (a b : Int) : ofInt (a - b) = ofInt a - ofInt b

@[simp]

theorem Int32.ofInt_sub (a b : Int) : ofInt (a - b) = ofInt a - ofInt b

@[simp]

theorem Int64.ofInt_sub (a b : Int) : ofInt (a - b) = ofInt a - ofInt b

@[simp]

theorem ISize.ofInt_sub (a b : Int) : ofInt (a - b) = ofInt a - ofInt b

@[simp]

theorem Int8.ofNat_sub (a b : Nat) (hab : b ≤ a) : ofNat (a - b) = ofNat a - ofNat b

@[simp]

theorem Int16.ofNat_sub (a b : Nat) (hab : b ≤ a) : ofNat (a - b) = ofNat a - ofNat b

@[simp]

theorem Int32.ofNat_sub (a b : Nat) (hab : b ≤ a) : ofNat (a - b) = ofNat a - ofNat b

@[simp]

theorem Int64.ofNat_sub (a b : Nat) (hab : b ≤ a) : ofNat (a - b) = ofNat a - ofNat b

@[simp]

theorem ISize.ofNat_sub (a b : Nat) (hab : b ≤ a) : ofNat (a - b) = ofNat a - ofNat b

theorem Int8.ofIntLE_sub {a b : Int} {hab₁ : minValue.toInt ≤ a - b} {hab₂ : a - b ≤ maxValue.toInt} : ofIntLE (a - b) hab₁ hab₂ = ofInt a - ofInt b

theorem Int16.ofIntLE_sub {a b : Int} {hab₁ : minValue.toInt ≤ a - b} {hab₂ : a - b ≤ maxValue.toInt} : ofIntLE (a - b) hab₁ hab₂ = ofInt a - ofInt b

theorem Int32.ofIntLE_sub {a b : Int} {hab₁ : minValue.toInt ≤ a - b} {hab₂ : a - b ≤ maxValue.toInt} : ofIntLE (a - b) hab₁ hab₂ = ofInt a - ofInt b

theorem Int64.ofIntLE_sub {a b : Int} {hab₁ : minValue.toInt ≤ a - b} {hab₂ : a - b ≤ maxValue.toInt} : ofIntLE (a - b) hab₁ hab₂ = ofInt a - ofInt b

theorem ISize.ofIntLE_sub {a b : Int} {hab₁ : minValue.toInt ≤ a - b} {hab₂ : a - b ≤ maxValue.toInt} : ofIntLE (a - b) hab₁ hab₂ = ofInt a - ofInt b

@[simp]

theorem Int8.ofBitVec_mul (a b : BitVec 8) : ofBitVec (a * b) = ofBitVec a * ofBitVec b

@[simp]

theorem Int16.ofBitVec_mul (a b : BitVec 16) : ofBitVec (a * b) = ofBitVec a * ofBitVec b

@[simp]

theorem Int32.ofBitVec_mul (a b : BitVec 32) : ofBitVec (a * b) = ofBitVec a * ofBitVec b

@[simp]

theorem Int64.ofBitVec_mul (a b : BitVec 64) : ofBitVec (a * b) = ofBitVec a * ofBitVec b

@[simp]

theorem ISize.ofBitVec_mul (a b : BitVec System.Platform.numBits) : ofBitVec (a * b) = ofBitVec a * ofBitVec b

@[simp]

theorem Int8.ofInt_mul (a b : Int) : ofInt (a * b) = ofInt a * ofInt b

@[simp]

theorem Int16.ofInt_mul (a b : Int) : ofInt (a * b) = ofInt a * ofInt b

@[simp]

theorem Int32.ofInt_mul (a b : Int) : ofInt (a * b) = ofInt a * ofInt b

@[simp]

theorem Int64.ofInt_mul (a b : Int) : ofInt (a * b) = ofInt a * ofInt b

@[simp]

theorem ISize.ofInt_mul (a b : Int) : ofInt (a * b) = ofInt a * ofInt b

@[simp]

theorem Int8.ofNat_mul (a b : Nat) : ofNat (a * b) = ofNat a * ofNat b

@[simp]

theorem Int16.ofNat_mul (a b : Nat) : ofNat (a * b) = ofNat a * ofNat b

@[simp]

theorem Int32.ofNat_mul (a b : Nat) : ofNat (a * b) = ofNat a * ofNat b

@[simp]

theorem Int64.ofNat_mul (a b : Nat) : ofNat (a * b) = ofNat a * ofNat b

@[simp]

theorem ISize.ofNat_mul (a b : Nat) : ofNat (a * b) = ofNat a * ofNat b

theorem Int8.ofIntLE_mul {a b : Int} {hab₁ : minValue.toInt ≤ a * b} {hab₂ : a * b ≤ maxValue.toInt} : ofIntLE (a * b) hab₁ hab₂ = ofInt a * ofInt b

theorem Int16.ofIntLE_mul {a b : Int} {hab₁ : minValue.toInt ≤ a * b} {hab₂ : a * b ≤ maxValue.toInt} : ofIntLE (a * b) hab₁ hab₂ = ofInt a * ofInt b

theorem Int32.ofIntLE_mul {a b : Int} {hab₁ : minValue.toInt ≤ a * b} {hab₂ : a * b ≤ maxValue.toInt} : ofIntLE (a * b) hab₁ hab₂ = ofInt a * ofInt b

theorem Int64.ofIntLE_mul {a b : Int} {hab₁ : minValue.toInt ≤ a * b} {hab₂ : a * b ≤ maxValue.toInt} : ofIntLE (a * b) hab₁ hab₂ = ofInt a * ofInt b

theorem ISize.ofIntLE_mul {a b : Int} {hab₁ : minValue.toInt ≤ a * b} {hab₂ : a * b ≤ maxValue.toInt} : ofIntLE (a * b) hab₁ hab₂ = ofInt a * ofInt b

theorem Int8.toInt_minValue_lt_zero : minValue.toInt < 0

theorem Int16.toInt_minValue_lt_zero : minValue.toInt < 0

theorem Int32.toInt_minValue_lt_zero : minValue.toInt < 0

theorem Int64.toInt_minValue_lt_zero : minValue.toInt < 0

theorem ISize.toInt_minValue_lt_zero : minValue.toInt < 0

theorem Int8.toInt_maxValue_add_one : maxValue.toInt + 1 = 2 ^ 7

theorem Int16.toInt_maxValue_add_one : maxValue.toInt + 1 = 2 ^ 15

theorem Int32.toInt_maxValue_add_one : maxValue.toInt + 1 = 2 ^ 31

theorem Int64.toInt_maxValue_add_one : maxValue.toInt + 1 = 2 ^ 63

theorem ISize.toInt_maxValue_add_one : maxValue.toInt + 1 = 2 ^ (System.Platform.numBits - 1)

@[simp]

theorem Int8.ofBitVec_sdiv (a b : BitVec 8) : ofBitVec (a.sdiv b) = ofBitVec a / ofBitVec b

@[simp]

theorem Int16.ofBitVec_sdiv (a b : BitVec 16) : ofBitVec (a.sdiv b) = ofBitVec a / ofBitVec b

@[simp]

theorem Int32.ofBitVec_sdiv (a b : BitVec 32) : ofBitVec (a.sdiv b) = ofBitVec a / ofBitVec b

@[simp]

theorem Int64.ofBitVec_sdiv (a b : BitVec 64) : ofBitVec (a.sdiv b) = ofBitVec a / ofBitVec b

@[simp]

theorem ISize.ofBitVec_sdiv (a b : BitVec System.Platform.numBits) : ofBitVec (a.sdiv b) = ofBitVec a / ofBitVec b

theorem Int8.ofInt_tdiv {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofInt (a.tdiv b) = ofInt a / ofInt b

theorem Int16.ofInt_tdiv {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofInt (a.tdiv b) = ofInt a / ofInt b

theorem Int32.ofInt_tdiv {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofInt (a.tdiv b) = ofInt a / ofInt b

theorem Int64.ofInt_tdiv {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofInt (a.tdiv b) = ofInt a / ofInt b

theorem ISize.ofInt_tdiv {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofInt (a.tdiv b) = ofInt a / ofInt b

theorem Int8.ofInt_eq_ofIntLE_div {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofInt (a.tdiv b) = ofIntLE a ha₁ ha₂ / ofIntLE b hb₁ hb₂

theorem Int16.ofInt_eq_ofIntLE_div {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofInt (a.tdiv b) = ofIntLE a ha₁ ha₂ / ofIntLE b hb₁ hb₂

theorem Int32.ofInt_eq_ofIntLE_div {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofInt (a.tdiv b) = ofIntLE a ha₁ ha₂ / ofIntLE b hb₁ hb₂

theorem Int64.ofInt_eq_ofIntLE_div {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofInt (a.tdiv b) = ofIntLE a ha₁ ha₂ / ofIntLE b hb₁ hb₂

theorem ISize.ofInt_eq_ofIntLE_div {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofInt (a.tdiv b) = ofIntLE a ha₁ ha₂ / ofIntLE b hb₁ hb₂

theorem Int8.ofNat_div {a b : Nat} (ha : a < 2 ^ 7) (hb : b < 2 ^ 7) : ofNat (a / b) = ofNat a / ofNat b

theorem Int16.ofNat_div {a b : Nat} (ha : a < 2 ^ 15) (hb : b < 2 ^ 15) : ofNat (a / b) = ofNat a / ofNat b

theorem Int32.ofNat_div {a b : Nat} (ha : a < 2 ^ 31) (hb : b < 2 ^ 31) : ofNat (a / b) = ofNat a / ofNat b

theorem Int64.ofNat_div {a b : Nat} (ha : a < 2 ^ 63) (hb : b < 2 ^ 63) : ofNat (a / b) = ofNat a / ofNat b

theorem ISize.ofNat_div {a b : Nat} (ha : a < 2 ^ (System.Platform.numBits - 1)) (hb : b < 2 ^ (System.Platform.numBits - 1)) : ofNat (a / b) = ofNat a / ofNat b

@[simp]

theorem Int8.ofBitVec_srem (a b : BitVec 8) : ofBitVec (a.srem b) = ofBitVec a % ofBitVec b

@[simp]

theorem Int16.ofBitVec_srem (a b : BitVec 16) : ofBitVec (a.srem b) = ofBitVec a % ofBitVec b

@[simp]

theorem Int32.ofBitVec_srem (a b : BitVec 32) : ofBitVec (a.srem b) = ofBitVec a % ofBitVec b

@[simp]

theorem Int64.ofBitVec_srem (a b : BitVec 64) : ofBitVec (a.srem b) = ofBitVec a % ofBitVec b

@[simp]

theorem ISize.ofBitVec_srem (a b : BitVec System.Platform.numBits) : ofBitVec (a.srem b) = ofBitVec a % ofBitVec b

@[simp]

theorem Int8.toInt_bmod_size (a : Int8) : a.toInt.bmod size = a.toInt

@[simp]

theorem Int16.toInt_bmod_size (a : Int16) : a.toInt.bmod size = a.toInt

@[simp]

theorem Int32.toInt_bmod_size (a : Int32) : a.toInt.bmod size = a.toInt

@[simp]

theorem Int64.toInt_bmod_size (a : Int64) : a.toInt.bmod size = a.toInt

@[simp]

theorem ISize.toInt_bmod_size (a : ISize) : a.toInt.bmod size = a.toInt

theorem Int8.ofIntLE_le_iff_le {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofIntLE a ha₁ ha₂ ≤ ofIntLE b hb₁ hb₂ ↔ a ≤ b

theorem Int16.ofIntLE_le_iff_le {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofIntLE a ha₁ ha₂ ≤ ofIntLE b hb₁ hb₂ ↔ a ≤ b

theorem Int32.ofIntLE_le_iff_le {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofIntLE a ha₁ ha₂ ≤ ofIntLE b hb₁ hb₂ ↔ a ≤ b

theorem Int64.ofIntLE_le_iff_le {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofIntLE a ha₁ ha₂ ≤ ofIntLE b hb₁ hb₂ ↔ a ≤ b

theorem ISize.ofIntLE_le_iff_le {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofIntLE a ha₁ ha₂ ≤ ofIntLE b hb₁ hb₂ ↔ a ≤ b

theorem Int8.ofInt_le_iff_le {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofInt a ≤ ofInt b ↔ a ≤ b

theorem Int16.ofInt_le_iff_le {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofInt a ≤ ofInt b ↔ a ≤ b

theorem Int32.ofInt_le_iff_le {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofInt a ≤ ofInt b ↔ a ≤ b

theorem Int64.ofInt_le_iff_le {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofInt a ≤ ofInt b ↔ a ≤ b

theorem ISize.ofInt_le_iff_le {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofInt a ≤ ofInt b ↔ a ≤ b

theorem Int8.ofNat_le_iff_le {a b : Nat} (ha : a < 2 ^ 7) (hb : b < 2 ^ 7) : ofNat a ≤ ofNat b ↔ a ≤ b

theorem Int16.ofNat_le_iff_le {a b : Nat} (ha : a < 2 ^ 15) (hb : b < 2 ^ 15) : ofNat a ≤ ofNat b ↔ a ≤ b

theorem Int32.ofNat_le_iff_le {a b : Nat} (ha : a < 2 ^ 31) (hb : b < 2 ^ 31) : ofNat a ≤ ofNat b ↔ a ≤ b

theorem Int64.ofNat_le_iff_le {a b : Nat} (ha : a < 2 ^ 63) (hb : b < 2 ^ 63) : ofNat a ≤ ofNat b ↔ a ≤ b

theorem ISize.ofNat_le_iff_le {a b : Nat} (ha : a < 2 ^ (System.Platform.numBits - 1)) (hb : b < 2 ^ (System.Platform.numBits - 1)) : ofNat a ≤ ofNat b ↔ a ≤ b

theorem Int8.ofBitVec_le_iff_sle (a b : BitVec 8) : ofBitVec a ≤ ofBitVec b ↔ a.sle b = true

theorem Int16.ofBitVec_le_iff_sle (a b : BitVec 16) : ofBitVec a ≤ ofBitVec b ↔ a.sle b = true

theorem Int32.ofBitVec_le_iff_sle (a b : BitVec 32) : ofBitVec a ≤ ofBitVec b ↔ a.sle b = true

theorem Int64.ofBitVec_le_iff_sle (a b : BitVec 64) : ofBitVec a ≤ ofBitVec b ↔ a.sle b = true

theorem ISize.ofBitVec_le_iff_sle (a b : BitVec System.Platform.numBits) : ofBitVec a ≤ ofBitVec b ↔ a.sle b = true

theorem Int8.ofIntLE_lt_iff_lt {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofIntLE a ha₁ ha₂ < ofIntLE b hb₁ hb₂ ↔ a < b

theorem Int16.ofIntLE_lt_iff_lt {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofIntLE a ha₁ ha₂ < ofIntLE b hb₁ hb₂ ↔ a < b

theorem Int32.ofIntLE_lt_iff_lt {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofIntLE a ha₁ ha₂ < ofIntLE b hb₁ hb₂ ↔ a < b

theorem Int64.ofIntLE_lt_iff_lt {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofIntLE a ha₁ ha₂ < ofIntLE b hb₁ hb₂ ↔ a < b

theorem ISize.ofIntLE_lt_iff_lt {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofIntLE a ha₁ ha₂ < ofIntLE b hb₁ hb₂ ↔ a < b

theorem Int8.ofInt_lt_iff_lt {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofInt a < ofInt b ↔ a < b

theorem Int16.ofInt_lt_iff_lt {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofInt a < ofInt b ↔ a < b

theorem Int32.ofInt_lt_iff_lt {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofInt a < ofInt b ↔ a < b

theorem Int64.ofInt_lt_iff_lt {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofInt a < ofInt b ↔ a < b

theorem ISize.ofInt_lt_iff_lt {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofInt a < ofInt b ↔ a < b

theorem Int8.ofNat_lt_iff_lt {a b : Nat} (ha : a < 2 ^ 7) (hb : b < 2 ^ 7) : ofNat a < ofNat b ↔ a < b

theorem Int16.ofNat_lt_iff_lt {a b : Nat} (ha : a < 2 ^ 15) (hb : b < 2 ^ 15) : ofNat a < ofNat b ↔ a < b

theorem Int32.ofNat_lt_iff_lt {a b : Nat} (ha : a < 2 ^ 31) (hb : b < 2 ^ 31) : ofNat a < ofNat b ↔ a < b

theorem Int64.ofNat_lt_iff_lt {a b : Nat} (ha : a < 2 ^ 63) (hb : b < 2 ^ 63) : ofNat a < ofNat b ↔ a < b

theorem ISize.ofNat_lt_iff_lt {a b : Nat} (ha : a < 2 ^ (System.Platform.numBits - 1)) (hb : b < 2 ^ (System.Platform.numBits - 1)) : ofNat a < ofNat b ↔ a < b

theorem Int8.ofBitVec_lt_iff_slt (a b : BitVec 8) : ofBitVec a < ofBitVec b ↔ a.slt b = true

theorem Int16.ofBitVec_lt_iff_slt (a b : BitVec 16) : ofBitVec a < ofBitVec b ↔ a.slt b = true

theorem Int32.ofBitVec_lt_iff_slt (a b : BitVec 32) : ofBitVec a < ofBitVec b ↔ a.slt b = true

theorem Int64.ofBitVec_lt_iff_slt (a b : BitVec 64) : ofBitVec a < ofBitVec b ↔ a.slt b = true

theorem ISize.ofBitVec_lt_iff_slt (a b : BitVec System.Platform.numBits) : ofBitVec a < ofBitVec b ↔ a.slt b = true

theorem Int8.toNatClampNeg_one : toNatClampNeg 1 = 1

theorem Int16.toNatClampNeg_one : toNatClampNeg 1 = 1

theorem Int32.toNatClampNeg_one : toNatClampNeg 1 = 1

theorem Int64.toNatClampNeg_one : toNatClampNeg 1 = 1

theorem ISize.toNatClampNeg_one : toNatClampNeg 1 = 1

theorem Int8.toInt_one : toInt 1 = 1

theorem Int16.toInt_one : toInt 1 = 1

theorem Int32.toInt_one : toInt 1 = 1

theorem Int64.toInt_one : toInt 1 = 1

theorem ISize.toInt_one : toInt 1 = 1

theorem Int8.zero_lt_one : 0 < 1

theorem Int16.zero_lt_one : 0 < 1

theorem Int32.zero_lt_one : 0 < 1

theorem Int64.zero_lt_one : 0 < 1

theorem ISize.zero_lt_one : 0 < 1

theorem Int8.zero_ne_one : 0 ≠ 1

theorem Int16.zero_ne_one : 0 ≠ 1

theorem Int32.zero_ne_one : 0 ≠ 1

theorem Int64.zero_ne_one : 0 ≠ 1

theorem ISize.zero_ne_one : 0 ≠ 1

theorem Int8.add_assoc (a b c : Int8) : a + b + c = a + (b + c)

theorem Int16.add_assoc (a b c : Int16) : a + b + c = a + (b + c)

theorem Int32.add_assoc (a b c : Int32) : a + b + c = a + (b + c)

theorem Int64.add_assoc (a b c : Int64) : a + b + c = a + (b + c)

theorem ISize.add_assoc (a b c : ISize) : a + b + c = a + (b + c)

instance instAssociativeInt8HAdd : Std.Associative fun (x1 x2 : Int8) => x1 + x2

instance instAssociativeInt16HAdd : Std.Associative fun (x1 x2 : Int16) => x1 + x2

instance instAssociativeInt32HAdd : Std.Associative fun (x1 x2 : Int32) => x1 + x2

instance instAssociativeInt64HAdd : Std.Associative fun (x1 x2 : Int64) => x1 + x2

instance instAssociativeISizeHAdd : Std.Associative fun (x1 x2 : ISize) => x1 + x2

theorem Int8.add_comm (a b : Int8) : a + b = b + a

theorem Int16.add_comm (a b : Int16) : a + b = b + a

theorem Int32.add_comm (a b : Int32) : a + b = b + a

theorem Int64.add_comm (a b : Int64) : a + b = b + a

theorem ISize.add_comm (a b : ISize) : a + b = b + a

instance instCommutativeInt8HAdd : Std.Commutative fun (x1 x2 : Int8) => x1 + x2

instance instCommutativeInt16HAdd : Std.Commutative fun (x1 x2 : Int16) => x1 + x2

instance instCommutativeInt32HAdd : Std.Commutative fun (x1 x2 : Int32) => x1 + x2

instance instCommutativeInt64HAdd : Std.Commutative fun (x1 x2 : Int64) => x1 + x2

instance instCommutativeISizeHAdd : Std.Commutative fun (x1 x2 : ISize) => x1 + x2

@[simp]

theorem Int8.add_zero (a : Int8) : a + 0 = a

@[simp]

theorem Int16.add_zero (a : Int16) : a + 0 = a

@[simp]

theorem Int32.add_zero (a : Int32) : a + 0 = a

@[simp]

theorem Int64.add_zero (a : Int64) : a + 0 = a

@[simp]

theorem ISize.add_zero (a : ISize) : a + 0 = a

@[simp]

theorem Int8.zero_add (a : Int8) : 0 + a = a

@[simp]

theorem Int16.zero_add (a : Int16) : 0 + a = a

@[simp]

theorem Int32.zero_add (a : Int32) : 0 + a = a

@[simp]

theorem Int64.zero_add (a : Int64) : 0 + a = a

@[simp]

theorem ISize.zero_add (a : ISize) : 0 + a = a

instance instLawfulIdentityInt8HAddOfNat : Std.LawfulIdentity (fun (x1 x2 : Int8) => x1 + x2) 0

instance instLawfulIdentityInt16HAddOfNat : Std.LawfulIdentity (fun (x1 x2 : Int16) => x1 + x2) 0

instance instLawfulIdentityInt32HAddOfNat : Std.LawfulIdentity (fun (x1 x2 : Int32) => x1 + x2) 0

instance instLawfulIdentityInt64HAddOfNat : Std.LawfulIdentity (fun (x1 x2 : Int64) => x1 + x2) 0

instance instLawfulIdentityISizeHAddOfNat : Std.LawfulIdentity (fun (x1 x2 : ISize) => x1 + x2) 0

@[simp]

theorem Int8.sub_zero (a : Int8) : a - 0 = a

@[simp]

theorem Int16.sub_zero (a : Int16) : a - 0 = a

@[simp]

theorem Int32.sub_zero (a : Int32) : a - 0 = a

@[simp]

theorem Int64.sub_zero (a : Int64) : a - 0 = a

@[simp]

theorem ISize.sub_zero (a : ISize) : a - 0 = a

@[simp]

theorem Int8.zero_sub (a : Int8) : 0 - a = -a

@[simp]

theorem Int16.zero_sub (a : Int16) : 0 - a = -a

@[simp]

theorem Int32.zero_sub (a : Int32) : 0 - a = -a

@[simp]

theorem Int64.zero_sub (a : Int64) : 0 - a = -a

@[simp]

theorem ISize.zero_sub (a : ISize) : 0 - a = -a

@[simp]

theorem Int8.sub_self (a : Int8) : a - a = 0

@[simp]

theorem Int16.sub_self (a : Int16) : a - a = 0

@[simp]

theorem Int32.sub_self (a : Int32) : a - a = 0

@[simp]

theorem Int64.sub_self (a : Int64) : a - a = 0

@[simp]

theorem ISize.sub_self (a : ISize) : a - a = 0

theorem Int8.add_left_neg (a : Int8) : -a + a = 0

theorem Int8.add_right_neg (a : Int8) : a + -a = 0

theorem Int16.add_left_neg (a : Int16) : -a + a = 0

theorem Int16.add_right_neg (a : Int16) : a + -a = 0

theorem Int32.add_left_neg (a : Int32) : -a + a = 0

theorem Int32.add_right_neg (a : Int32) : a + -a = 0

theorem Int64.add_left_neg (a : Int64) : -a + a = 0

theorem Int64.add_right_neg (a : Int64) : a + -a = 0

theorem ISize.add_left_neg (a : ISize) : -a + a = 0

theorem ISize.add_right_neg (a : ISize) : a + -a = 0

@[simp]

theorem Int8.sub_add_cancel (a b : Int8) : a - b + b = a

@[simp]

theorem Int16.sub_add_cancel (a b : Int16) : a - b + b = a

@[simp]

theorem Int32.sub_add_cancel (a b : Int32) : a - b + b = a

@[simp]

theorem Int64.sub_add_cancel (a b : Int64) : a - b + b = a

@[simp]

theorem ISize.sub_add_cancel (a b : ISize) : a - b + b = a

theorem Int8.eq_sub_iff_add_eq {a b c : Int8} : a = c - b ↔ a + b = c

theorem Int16.eq_sub_iff_add_eq {a b c : Int16} : a = c - b ↔ a + b = c

theorem Int32.eq_sub_iff_add_eq {a b c : Int32} : a = c - b ↔ a + b = c

theorem Int64.eq_sub_iff_add_eq {a b c : Int64} : a = c - b ↔ a + b = c

theorem ISize.eq_sub_iff_add_eq {a b c : ISize} : a = c - b ↔ a + b = c

theorem Int8.sub_eq_iff_eq_add {a b c : Int8} : a - b = c ↔ a = c + b

theorem Int16.sub_eq_iff_eq_add {a b c : Int16} : a - b = c ↔ a = c + b

theorem Int32.sub_eq_iff_eq_add {a b c : Int32} : a - b = c ↔ a = c + b

theorem Int64.sub_eq_iff_eq_add {a b c : Int64} : a - b = c ↔ a = c + b

theorem ISize.sub_eq_iff_eq_add {a b c : ISize} : a - b = c ↔ a = c + b

@[simp]

theorem Int8.neg_neg {a : Int8} : - -a = a

@[simp]

theorem Int16.neg_neg {a : Int16} : - -a = a

@[simp]

theorem Int32.neg_neg {a : Int32} : - -a = a

@[simp]

theorem Int64.neg_neg {a : Int64} : - -a = a

@[simp]

theorem ISize.neg_neg {a : ISize} : - -a = a

@[simp]

theorem Int8.neg_inj {a b : Int8} : -a = -b ↔ a = b

@[simp]

theorem Int16.neg_inj {a b : Int16} : -a = -b ↔ a = b

@[simp]

theorem Int32.neg_inj {a b : Int32} : -a = -b ↔ a = b

@[simp]

theorem Int64.neg_inj {a b : Int64} : -a = -b ↔ a = b

@[simp]

theorem ISize.neg_inj {a b : ISize} : -a = -b ↔ a = b

@[simp]

theorem Int8.neg_ne_zero {a : Int8} : -a ≠ 0 ↔ a ≠ 0

@[simp]

theorem Int16.neg_ne_zero {a : Int16} : -a ≠ 0 ↔ a ≠ 0

@[simp]

theorem Int32.neg_ne_zero {a : Int32} : -a ≠ 0 ↔ a ≠ 0

@[simp]

theorem Int64.neg_ne_zero {a : Int64} : -a ≠ 0 ↔ a ≠ 0

@[simp]

theorem ISize.neg_ne_zero {a : ISize} : -a ≠ 0 ↔ a ≠ 0

theorem Int8.neg_add {a b : Int8} : -(a + b) = -a - b

theorem Int16.neg_add {a b : Int16} : -(a + b) = -a - b

theorem Int32.neg_add {a b : Int32} : -(a + b) = -a - b

theorem Int64.neg_add {a b : Int64} : -(a + b) = -a - b

theorem ISize.neg_add {a b : ISize} : -(a + b) = -a - b

@[simp]

theorem Int8.sub_neg {a b : Int8} : a - -b = a + b

@[simp]

theorem Int16.sub_neg {a b : Int16} : a - -b = a + b

@[simp]

theorem Int32.sub_neg {a b : Int32} : a - -b = a + b

@[simp]

theorem Int64.sub_neg {a b : Int64} : a - -b = a + b

@[simp]

theorem ISize.sub_neg {a b : ISize} : a - -b = a + b

@[simp]

theorem Int8.neg_sub {a b : Int8} : -(a - b) = b - a

@[simp]

theorem Int16.neg_sub {a b : Int16} : -(a - b) = b - a

@[simp]

theorem Int32.neg_sub {a b : Int32} : -(a - b) = b - a

@[simp]

theorem Int64.neg_sub {a b : Int64} : -(a - b) = b - a

@[simp]

theorem ISize.neg_sub {a b : ISize} : -(a - b) = b - a

theorem Int8.sub_sub (a b c : Int8) : a - b - c = a - (b + c)

theorem Int16.sub_sub (a b c : Int16) : a - b - c = a - (b + c)

theorem Int32.sub_sub (a b c : Int32) : a - b - c = a - (b + c)

theorem Int64.sub_sub (a b c : Int64) : a - b - c = a - (b + c)

theorem ISize.sub_sub (a b c : ISize) : a - b - c = a - (b + c)

@[simp]

theorem Int8.add_left_inj {a b : Int8} (c : Int8) : a + c = b + c ↔ a = b

@[simp]

theorem Int16.add_left_inj {a b : Int16} (c : Int16) : a + c = b + c ↔ a = b

@[simp]

theorem Int32.add_left_inj {a b : Int32} (c : Int32) : a + c = b + c ↔ a = b

@[simp]

theorem Int64.add_left_inj {a b : Int64} (c : Int64) : a + c = b + c ↔ a = b

@[simp]

theorem ISize.add_left_inj {a b : ISize} (c : ISize) : a + c = b + c ↔ a = b

@[simp]

theorem Int8.add_right_inj {a b : Int8} (c : Int8) : c + a = c + b ↔ a = b

@[simp]

theorem Int16.add_right_inj {a b : Int16} (c : Int16) : c + a = c + b ↔ a = b

@[simp]

theorem Int32.add_right_inj {a b : Int32} (c : Int32) : c + a = c + b ↔ a = b

@[simp]

theorem Int64.add_right_inj {a b : Int64} (c : Int64) : c + a = c + b ↔ a = b

@[simp]

theorem ISize.add_right_inj {a b : ISize} (c : ISize) : c + a = c + b ↔ a = b

@[simp]

theorem Int8.sub_left_inj {a b : Int8} (c : Int8) : a - c = b - c ↔ a = b

@[simp]

theorem Int16.sub_left_inj {a b : Int16} (c : Int16) : a - c = b - c ↔ a = b

@[simp]

theorem Int32.sub_left_inj {a b : Int32} (c : Int32) : a - c = b - c ↔ a = b

@[simp]

theorem Int64.sub_left_inj {a b : Int64} (c : Int64) : a - c = b - c ↔ a = b

@[simp]

theorem ISize.sub_left_inj {a b : ISize} (c : ISize) : a - c = b - c ↔ a = b

@[simp]

theorem Int8.sub_right_inj {a b : Int8} (c : Int8) : c - a = c - b ↔ a = b

@[simp]

theorem Int16.sub_right_inj {a b : Int16} (c : Int16) : c - a = c - b ↔ a = b

@[simp]

theorem Int32.sub_right_inj {a b : Int32} (c : Int32) : c - a = c - b ↔ a = b

@[simp]

theorem Int64.sub_right_inj {a b : Int64} (c : Int64) : c - a = c - b ↔ a = b

@[simp]

theorem ISize.sub_right_inj {a b : ISize} (c : ISize) : c - a = c - b ↔ a = b

@[simp]

theorem Int8.add_eq_right {a b : Int8} : a + b = b ↔ a = 0

@[simp]

theorem Int16.add_eq_right {a b : Int16} : a + b = b ↔ a = 0

@[simp]

theorem Int32.add_eq_right {a b : Int32} : a + b = b ↔ a = 0

@[simp]

theorem Int64.add_eq_right {a b : Int64} : a + b = b ↔ a = 0

@[simp]

theorem ISize.add_eq_right {a b : ISize} : a + b = b ↔ a = 0

@[simp]

theorem Int8.add_eq_left {a b : Int8} : a + b = a ↔ b = 0

@[simp]

theorem Int16.add_eq_left {a b : Int16} : a + b = a ↔ b = 0

@[simp]

theorem Int32.add_eq_left {a b : Int32} : a + b = a ↔ b = 0

@[simp]

theorem Int64.add_eq_left {a b : Int64} : a + b = a ↔ b = 0

@[simp]

theorem ISize.add_eq_left {a b : ISize} : a + b = a ↔ b = 0

@[simp]

theorem Int8.right_eq_add {a b : Int8} : b = a + b ↔ a = 0

@[simp]

theorem Int16.right_eq_add {a b : Int16} : b = a + b ↔ a = 0

@[simp]

theorem Int32.right_eq_add {a b : Int32} : b = a + b ↔ a = 0

@[simp]

theorem Int64.right_eq_add {a b : Int64} : b = a + b ↔ a = 0

@[simp]

theorem ISize.right_eq_add {a b : ISize} : b = a + b ↔ a = 0

@[simp]

theorem Int8.left_eq_add {a b : Int8} : a = a + b ↔ b = 0

@[simp]

theorem Int16.left_eq_add {a b : Int16} : a = a + b ↔ b = 0

@[simp]

theorem Int32.left_eq_add {a b : Int32} : a = a + b ↔ b = 0

@[simp]

theorem Int64.left_eq_add {a b : Int64} : a = a + b ↔ b = 0

@[simp]

theorem ISize.left_eq_add {a b : ISize} : a = a + b ↔ b = 0

theorem Int8.mul_comm (a b : Int8) : a * b = b * a

theorem Int16.mul_comm (a b : Int16) : a * b = b * a

theorem Int32.mul_comm (a b : Int32) : a * b = b * a

theorem Int64.mul_comm (a b : Int64) : a * b = b * a

theorem ISize.mul_comm (a b : ISize) : a * b = b * a

instance instCommutativeInt8HMul : Std.Commutative fun (x1 x2 : Int8) => x1 * x2

instance instCommutativeInt16HMul : Std.Commutative fun (x1 x2 : Int16) => x1 * x2

instance instCommutativeInt32HMul : Std.Commutative fun (x1 x2 : Int32) => x1 * x2

instance instCommutativeInt64HMul : Std.Commutative fun (x1 x2 : Int64) => x1 * x2

instance instCommutativeISizeHMul : Std.Commutative fun (x1 x2 : ISize) => x1 * x2

theorem Int8.mul_assoc (a b c : Int8) : a * b * c = a * (b * c)

theorem Int16.mul_assoc (a b c : Int16) : a * b * c = a * (b * c)

theorem Int32.mul_assoc (a b c : Int32) : a * b * c = a * (b * c)

theorem Int64.mul_assoc (a b c : Int64) : a * b * c = a * (b * c)

theorem ISize.mul_assoc (a b c : ISize) : a * b * c = a * (b * c)

instance instAssociativeInt8HMul : Std.Associative fun (x1 x2 : Int8) => x1 * x2

instance instAssociativeInt16HMul : Std.Associative fun (x1 x2 : Int16) => x1 * x2

instance instAssociativeInt32HMul : Std.Associative fun (x1 x2 : Int32) => x1 * x2

instance instAssociativeInt64HMul : Std.Associative fun (x1 x2 : Int64) => x1 * x2

instance instAssociativeISizeHMul : Std.Associative fun (x1 x2 : ISize) => x1 * x2

@[simp]

theorem Int8.mul_one (a : Int8) : a * 1 = a

@[simp]

theorem Int16.mul_one (a : Int16) : a * 1 = a

@[simp]

theorem Int32.mul_one (a : Int32) : a * 1 = a

@[simp]

theorem Int64.mul_one (a : Int64) : a * 1 = a

@[simp]

theorem ISize.mul_one (a : ISize) : a * 1 = a

@[simp]

theorem Int8.one_mul (a : Int8) : 1 * a = a

@[simp]

theorem Int16.one_mul (a : Int16) : 1 * a = a

@[simp]

theorem Int32.one_mul (a : Int32) : 1 * a = a

@[simp]

theorem Int64.one_mul (a : Int64) : 1 * a = a

@[simp]

theorem ISize.one_mul (a : ISize) : 1 * a = a

instance instLawfulCommIdentityInt8HMulOfNat : Std.LawfulCommIdentity (fun (x1 x2 : Int8) => x1 * x2) 1

instance instLawfulCommIdentityInt16HMulOfNat : Std.LawfulCommIdentity (fun (x1 x2 : Int16) => x1 * x2) 1

instance instLawfulCommIdentityInt32HMulOfNat : Std.LawfulCommIdentity (fun (x1 x2 : Int32) => x1 * x2) 1

instance instLawfulCommIdentityInt64HMulOfNat : Std.LawfulCommIdentity (fun (x1 x2 : Int64) => x1 * x2) 1

instance instLawfulCommIdentityISizeHMulOfNat : Std.LawfulCommIdentity (fun (x1 x2 : ISize) => x1 * x2) 1

@[simp]

theorem Int8.mul_zero {a : Int8} : a * 0 = 0

@[simp]

theorem Int16.mul_zero {a : Int16} : a * 0 = 0

@[simp]

theorem Int32.mul_zero {a : Int32} : a * 0 = 0

@[simp]

theorem Int64.mul_zero {a : Int64} : a * 0 = 0

@[simp]

theorem ISize.mul_zero {a : ISize} : a * 0 = 0

@[simp]

theorem Int8.zero_mul {a : Int8} : 0 * a = 0

@[simp]

theorem Int16.zero_mul {a : Int16} : 0 * a = 0

@[simp]

theorem Int32.zero_mul {a : Int32} : 0 * a = 0

@[simp]

theorem Int64.zero_mul {a : Int64} : 0 * a = 0

@[simp]

theorem ISize.zero_mul {a : ISize} : 0 * a = 0

@[simp]

theorem Int8.pow_zero (x : Int8) : x ^ 0 = 1

theorem Int8.pow_succ (x : Int8) (n : Nat) : x ^ (n + 1) = x ^ n * x

@[simp]

theorem Int16.pow_zero (x : Int16) : x ^ 0 = 1

theorem Int16.pow_succ (x : Int16) (n : Nat) : x ^ (n + 1) = x ^ n * x

@[simp]

theorem Int32.pow_zero (x : Int32) : x ^ 0 = 1

theorem Int32.pow_succ (x : Int32) (n : Nat) : x ^ (n + 1) = x ^ n * x

@[simp]

theorem Int64.pow_zero (x : Int64) : x ^ 0 = 1

theorem Int64.pow_succ (x : Int64) (n : Nat) : x ^ (n + 1) = x ^ n * x

@[simp]

theorem ISize.pow_zero (x : ISize) : x ^ 0 = 1

theorem ISize.pow_succ (x : ISize) (n : Nat) : x ^ (n + 1) = x ^ n * x

theorem Int8.mul_add {a b c : Int8} : a * (b + c) = a * b + a * c

theorem Int16.mul_add {a b c : Int16} : a * (b + c) = a * b + a * c

theorem Int32.mul_add {a b c : Int32} : a * (b + c) = a * b + a * c

theorem Int64.mul_add {a b c : Int64} : a * (b + c) = a * b + a * c

theorem ISize.mul_add {a b c : ISize} : a * (b + c) = a * b + a * c

theorem Int8.add_mul {a b c : Int8} : (a + b) * c = a * c + b * c

theorem Int16.add_mul {a b c : Int16} : (a + b) * c = a * c + b * c

theorem Int32.add_mul {a b c : Int32} : (a + b) * c = a * c + b * c

theorem Int64.add_mul {a b c : Int64} : (a + b) * c = a * c + b * c

theorem ISize.add_mul {a b c : ISize} : (a + b) * c = a * c + b * c

theorem Int8.mul_succ {a b : Int8} : a * (b + 1) = a * b + a

theorem Int16.mul_succ {a b : Int16} : a * (b + 1) = a * b + a

theorem Int32.mul_succ {a b : Int32} : a * (b + 1) = a * b + a

theorem Int64.mul_succ {a b : Int64} : a * (b + 1) = a * b + a

theorem ISize.mul_succ {a b : ISize} : a * (b + 1) = a * b + a

theorem Int8.succ_mul {a b : Int8} : (a + 1) * b = a * b + b

theorem Int16.succ_mul {a b : Int16} : (a + 1) * b = a * b + b

theorem Int32.succ_mul {a b : Int32} : (a + 1) * b = a * b + b

theorem Int64.succ_mul {a b : Int64} : (a + 1) * b = a * b + b

theorem ISize.succ_mul {a b : ISize} : (a + 1) * b = a * b + b

theorem Int8.two_mul {a : Int8} : 2 * a = a + a

theorem Int16.two_mul {a : Int16} : 2 * a = a + a

theorem Int32.two_mul {a : Int32} : 2 * a = a + a

theorem Int64.two_mul {a : Int64} : 2 * a = a + a

theorem ISize.two_mul {a : ISize} : 2 * a = a + a

theorem Int8.mul_two {a : Int8} : a * 2 = a + a

theorem Int16.mul_two {a : Int16} : a * 2 = a + a

theorem Int32.mul_two {a : Int32} : a * 2 = a + a

theorem Int64.mul_two {a : Int64} : a * 2 = a + a

theorem ISize.mul_two {a : ISize} : a * 2 = a + a

theorem Int8.neg_mul (a b : Int8) : -a * b = -(a * b)

theorem Int16.neg_mul (a b : Int16) : -a * b = -(a * b)

theorem Int32.neg_mul (a b : Int32) : -a * b = -(a * b)

theorem Int64.neg_mul (a b : Int64) : -a * b = -(a * b)

theorem ISize.neg_mul (a b : ISize) : -a * b = -(a * b)

theorem Int8.mul_neg (a b : Int8) : a * -b = -(a * b)

theorem Int16.mul_neg (a b : Int16) : a * -b = -(a * b)

theorem Int32.mul_neg (a b : Int32) : a * -b = -(a * b)

theorem Int64.mul_neg (a b : Int64) : a * -b = -(a * b)

theorem ISize.mul_neg (a b : ISize) : a * -b = -(a * b)

theorem Int8.neg_mul_neg (a b : Int8) : -a * -b = a * b

theorem Int16.neg_mul_neg (a b : Int16) : -a * -b = a * b

theorem Int32.neg_mul_neg (a b : Int32) : -a * -b = a * b

theorem Int64.neg_mul_neg (a b : Int64) : -a * -b = a * b

theorem ISize.neg_mul_neg (a b : ISize) : -a * -b = a * b

theorem Int8.neg_mul_comm (a b : Int8) : -a * b = a * -b

theorem Int16.neg_mul_comm (a b : Int16) : -a * b = a * -b

theorem Int32.neg_mul_comm (a b : Int32) : -a * b = a * -b

theorem Int64.neg_mul_comm (a b : Int64) : -a * b = a * -b

theorem ISize.neg_mul_comm (a b : ISize) : -a * b = a * -b

theorem Int8.mul_sub {a b c : Int8} : a * (b - c) = a * b - a * c

theorem Int16.mul_sub {a b c : Int16} : a * (b - c) = a * b - a * c

theorem Int32.mul_sub {a b c : Int32} : a * (b - c) = a * b - a * c

theorem Int64.mul_sub {a b c : Int64} : a * (b - c) = a * b - a * c

theorem ISize.mul_sub {a b c : ISize} : a * (b - c) = a * b - a * c

theorem Int8.sub_mul {a b c : Int8} : (a - b) * c = a * c - b * c

theorem Int16.sub_mul {a b c : Int16} : (a - b) * c = a * c - b * c

theorem Int32.sub_mul {a b c : Int32} : (a - b) * c = a * c - b * c

theorem Int64.sub_mul {a b c : Int64} : (a - b) * c = a * c - b * c

theorem ISize.sub_mul {a b c : ISize} : (a - b) * c = a * c - b * c

theorem Int8.neg_add_mul_eq_mul_not {a b : Int8} : -(a + a * b) = a * ~~~b

theorem Int16.neg_add_mul_eq_mul_not {a b : Int16} : -(a + a * b) = a * ~~~b

theorem Int32.neg_add_mul_eq_mul_not {a b : Int32} : -(a + a * b) = a * ~~~b

theorem Int64.neg_add_mul_eq_mul_not {a b : Int64} : -(a + a * b) = a * ~~~b

theorem ISize.neg_add_mul_eq_mul_not {a b : ISize} : -(a + a * b) = a * ~~~b

theorem Int8.neg_mul_not_eq_add_mul {a b : Int8} : -(a * ~~~b) = a + a * b

theorem Int16.neg_mul_not_eq_add_mul {a b : Int16} : -(a * ~~~b) = a + a * b

theorem Int32.neg_mul_not_eq_add_mul {a b : Int32} : -(a * ~~~b) = a + a * b

theorem Int64.neg_mul_not_eq_add_mul {a b : Int64} : -(a * ~~~b) = a + a * b

theorem ISize.neg_mul_not_eq_add_mul {a b : ISize} : -(a * ~~~b) = a + a * b

theorem Int8.le_of_lt {a b : Int8} : a < b → a ≤ b

theorem Int16.le_of_lt {a b : Int16} : a < b → a ≤ b

theorem Int32.le_of_lt {a b : Int32} : a < b → a ≤ b

theorem Int64.le_of_lt {a b : Int64} : a < b → a ≤ b

theorem ISize.le_of_lt {a b : ISize} : a < b → a ≤ b

theorem Int8.lt_of_le_of_ne {a b : Int8} : a ≤ b → a ≠ b → a < b

theorem Int16.lt_of_le_of_ne {a b : Int16} : a ≤ b → a ≠ b → a < b

theorem Int32.lt_of_le_of_ne {a b : Int32} : a ≤ b → a ≠ b → a < b

theorem Int64.lt_of_le_of_ne {a b : Int64} : a ≤ b → a ≠ b → a < b

theorem ISize.lt_of_le_of_ne {a b : ISize} : a ≤ b → a ≠ b → a < b

theorem Int8.lt_iff_le_and_ne {a b : Int8} : a < b ↔ a ≤ b ∧ a ≠ b

theorem Int16.lt_iff_le_and_ne {a b : Int16} : a < b ↔ a ≤ b ∧ a ≠ b

theorem Int32.lt_iff_le_and_ne {a b : Int32} : a < b ↔ a ≤ b ∧ a ≠ b

theorem Int64.lt_iff_le_and_ne {a b : Int64} : a < b ↔ a ≤ b ∧ a ≠ b

theorem ISize.lt_iff_le_and_ne {a b : ISize} : a < b ↔ a ≤ b ∧ a ≠ b

@[simp]

theorem Int8.lt_irrefl {a : Int8} : ¬a < a

@[simp]

theorem Int16.lt_irrefl {a : Int16} : ¬a < a

@[simp]

theorem Int32.lt_irrefl {a : Int32} : ¬a < a

@[simp]

theorem Int64.lt_irrefl {a : Int64} : ¬a < a

@[simp]

theorem ISize.lt_irrefl {a : ISize} : ¬a < a

theorem Int8.lt_of_le_of_lt {a b c : Int8} : a ≤ b → b < c → a < c

theorem Int16.lt_of_le_of_lt {a b c : Int16} : a ≤ b → b < c → a < c

theorem Int32.lt_of_le_of_lt {a b c : Int32} : a ≤ b → b < c → a < c

theorem Int64.lt_of_le_of_lt {a b c : Int64} : a ≤ b → b < c → a < c

theorem ISize.lt_of_le_of_lt {a b c : ISize} : a ≤ b → b < c → a < c

theorem Int8.lt_of_lt_of_le {a b c : Int8} : a < b → b ≤ c → a < c

theorem Int16.lt_of_lt_of_le {a b c : Int16} : a < b → b ≤ c → a < c

theorem Int32.lt_of_lt_of_le {a b c : Int32} : a < b → b ≤ c → a < c

theorem Int64.lt_of_lt_of_le {a b c : Int64} : a < b → b ≤ c → a < c

theorem ISize.lt_of_lt_of_le {a b c : ISize} : a < b → b ≤ c → a < c

@[simp]

theorem Int8.minValue_le (a : Int8) : minValue ≤ a

@[simp]

theorem Int16.minValue_le (a : Int16) : minValue ≤ a

@[simp]

theorem Int32.minValue_le (a : Int32) : minValue ≤ a

@[simp]

theorem Int64.minValue_le (a : Int64) : minValue ≤ a

@[simp]

theorem ISize.minValue_le (a : ISize) : minValue ≤ a

@[simp]

theorem Int8.le_maxValue (a : Int8) : a ≤ maxValue

@[simp]

theorem Int16.le_maxValue (a : Int16) : a ≤ maxValue

@[simp]

theorem Int32.le_maxValue (a : Int32) : a ≤ maxValue

@[simp]

theorem Int64.le_maxValue (a : Int64) : a ≤ maxValue

@[simp]

theorem ISize.le_maxValue (a : ISize) : a ≤ maxValue

@[simp]

theorem Int8.not_lt_minValue {a : Int8} : ¬a < minValue

@[simp]

theorem Int16.not_lt_minValue {a : Int16} : ¬a < minValue

@[simp]

theorem Int32.not_lt_minValue {a : Int32} : ¬a < minValue

@[simp]

theorem Int64.not_lt_minValue {a : Int64} : ¬a < minValue

@[simp]

theorem ISize.not_lt_minValue {a : ISize} : ¬a < minValue

@[simp]

theorem Int8.not_maxValue_lt {a : Int8} : ¬maxValue < a

@[simp]

theorem Int16.not_maxValue_lt {a : Int16} : ¬maxValue < a

@[simp]

theorem Int32.not_maxValue_lt {a : Int32} : ¬maxValue < a

@[simp]

theorem Int64.not_maxValue_lt {a : Int64} : ¬maxValue < a

@[simp]

theorem ISize.not_maxValue_lt {a : ISize} : ¬maxValue < a

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

theorem Int8.le_antisymm {a b : Int8} : a ≤ b → b ≤ a → a = b

theorem Int16.le_antisymm {a b : Int16} : a ≤ b → b ≤ a → a = b

theorem Int32.le_antisymm {a b : Int32} : a ≤ b → b ≤ a → a = b

theorem Int64.le_antisymm {a b : Int64} : a ≤ b → b ≤ a → a = b

theorem ISize.le_antisymm {a b : ISize} : a ≤ b → b ≤ a → a = b

@[simp]

theorem Int8.le_minValue_iff {a : Int8} : a ≤ minValue ↔ a = minValue

@[simp]

theorem Int16.le_minValue_iff {a : Int16} : a ≤ minValue ↔ a = minValue

@[simp]

theorem Int32.le_minValue_iff {a : Int32} : a ≤ minValue ↔ a = minValue

@[simp]

theorem Int64.le_minValue_iff {a : Int64} : a ≤ minValue ↔ a = minValue

@[simp]

theorem ISize.le_minValue_iff {a : ISize} : a ≤ minValue ↔ a = minValue

@[simp]

theorem Int8.maxValue_le_iff {a : Int8} : maxValue ≤ a ↔ a = maxValue

@[simp]

theorem Int16.maxValue_le_iff {a : Int16} : maxValue ≤ a ↔ a = maxValue

@[simp]

theorem Int32.maxValue_le_iff {a : Int32} : maxValue ≤ a ↔ a = maxValue

@[simp]

theorem Int64.maxValue_le_iff {a : Int64} : maxValue ≤ a ↔ a = maxValue

@[simp]

theorem ISize.maxValue_le_iff {a : ISize} : maxValue ≤ a ↔ a = maxValue

@[simp]

theorem Int8.zero_div {a : Int8} : 0 / a = 0

@[simp]

theorem Int16.zero_div {a : Int16} : 0 / a = 0

@[simp]

theorem Int32.zero_div {a : Int32} : 0 / a = 0

@[simp]

theorem Int64.zero_div {a : Int64} : 0 / a = 0

@[simp]

theorem ISize.zero_div {a : ISize} : 0 / a = 0

@[simp]

theorem Int8.div_zero {a : Int8} : a / 0 = 0

@[simp]

theorem Int16.div_zero {a : Int16} : a / 0 = 0

@[simp]

theorem Int32.div_zero {a : Int32} : a / 0 = 0

@[simp]

theorem Int64.div_zero {a : Int64} : a / 0 = 0

@[simp]

theorem ISize.div_zero {a : ISize} : a / 0 = 0

@[simp]

theorem Int8.div_one {a : Int8} : a / 1 = a

@[simp]

theorem Int16.div_one {a : Int16} : a / 1 = a

@[simp]

theorem Int32.div_one {a : Int32} : a / 1 = a

@[simp]

theorem Int64.div_one {a : Int64} : a / 1 = a

@[simp]

theorem ISize.div_one {a : ISize} : a / 1 = a

theorem Int8.div_self {a : Int8} : a / a = if a = 0 then 0 else 1

theorem Int16.div_self {a : Int16} : a / a = if a = 0 then 0 else 1

theorem Int32.div_self {a : Int32} : a / a = if a = 0 then 0 else 1

theorem Int64.div_self {a : Int64} : a / a = if a = 0 then 0 else 1

theorem ISize.div_self {a : ISize} : a / a = if a = 0 then 0 else 1

@[simp]

theorem Int8.mod_zero {a : Int8} : a % 0 = a

@[simp]

theorem Int16.mod_zero {a : Int16} : a % 0 = a

@[simp]

theorem Int32.mod_zero {a : Int32} : a % 0 = a

@[simp]

theorem Int64.mod_zero {a : Int64} : a % 0 = a

@[simp]

theorem ISize.mod_zero {a : ISize} : a % 0 = a

@[simp]

theorem Int8.zero_mod {a : Int8} : 0 % a = 0

@[simp]

theorem Int16.zero_mod {a : Int16} : 0 % a = 0

@[simp]

theorem Int32.zero_mod {a : Int32} : 0 % a = 0

@[simp]

theorem Int64.zero_mod {a : Int64} : 0 % a = 0

@[simp]

theorem ISize.zero_mod {a : ISize} : 0 % a = 0

@[simp]

theorem Int8.mod_one {a : Int8} : a % 1 = 0

@[simp]

theorem Int16.mod_one {a : Int16} : a % 1 = 0

@[simp]

theorem Int32.mod_one {a : Int32} : a % 1 = 0

@[simp]

theorem Int64.mod_one {a : Int64} : a % 1 = 0

@[simp]

theorem ISize.mod_one {a : ISize} : a % 1 = 0

@[simp]

theorem Int8.mod_self {a : Int8} : a % a = 0

@[simp]

theorem Int16.mod_self {a : Int16} : a % a = 0

@[simp]

theorem Int32.mod_self {a : Int32} : a % a = 0

@[simp]

theorem Int64.mod_self {a : Int64} : a % a = 0

@[simp]

theorem ISize.mod_self {a : ISize} : a % a = 0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

instance Int8.instIsLinearOrder : Std.IsLinearOrder Int8

instance instLawfulOrderLTInt8 : Std.LawfulOrderLT Int8

instance Int16.instIsLinearOrder : Std.IsLinearOrder Int16

instance instLawfulOrderLTInt16 : Std.LawfulOrderLT Int16

instance Int32.instIsLinearOrder : Std.IsLinearOrder Int32

instance instLawfulOrderLTInt32 : Std.LawfulOrderLT Int32

instance Int64.instIsLinearOrder : Std.IsLinearOrder Int64

instance instLawfulOrderLTInt64 : Std.LawfulOrderLT Int64

instance ISize.instIsLinearOrder : Std.IsLinearOrder ISize

instance instLawfulOrderLTISize : Std.LawfulOrderLT ISize

theorem Int8.add_neg_eq_sub {a b : Int8} : a + -b = a - b

theorem Int16.add_neg_eq_sub {a b : Int16} : a + -b = a - b

theorem Int32.add_neg_eq_sub {a b : Int32} : a + -b = a - b

theorem Int64.add_neg_eq_sub {a b : Int64} : a + -b = a - b

theorem ISize.add_neg_eq_sub {a b : ISize} : a + -b = a - b

theorem Int8.neg_eq_neg_one_mul (a : Int8) : -a = -1 * a

theorem Int16.neg_eq_neg_one_mul (a : Int16) : -a = -1 * a

theorem Int32.neg_eq_neg_one_mul (a : Int32) : -a = -1 * a

theorem Int64.neg_eq_neg_one_mul (a : Int64) : -a = -1 * a

theorem ISize.neg_eq_neg_one_mul (a : ISize) : -a = -1 * a

@[simp]

theorem Int8.add_sub_cancel (a b : Int8) : a + b - b = a

@[simp]

theorem Int16.add_sub_cancel (a b : Int16) : a + b - b = a

@[simp]

theorem Int32.add_sub_cancel (a b : Int32) : a + b - b = a

@[simp]

theorem Int64.add_sub_cancel (a b : Int64) : a + b - b = a

@[simp]

theorem ISize.add_sub_cancel (a b : ISize) : a + b - b = a

theorem Int8.lt_or_lt_of_ne {a b : Int8} : a ≠ b → a < b ∨ b < a

theorem Int16.lt_or_lt_of_ne {a b : Int16} : a ≠ b → a < b ∨ b < a

theorem Int32.lt_or_lt_of_ne {a b : Int32} : a ≠ b → a < b ∨ b < a

theorem Int64.lt_or_lt_of_ne {a b : Int64} : a ≠ b → a < b ∨ b < a

theorem ISize.lt_or_lt_of_ne {a b : ISize} : a ≠ b → a < b ∨ b < a

theorem Int8.lt_or_le (a b : Int8) : a < b ∨ b ≤ a

theorem Int16.lt_or_le (a b : Int16) : a < b ∨ b ≤ a

theorem Int32.lt_or_le (a b : Int32) : a < b ∨ b ≤ a

theorem Int64.lt_or_le (a b : Int64) : a < b ∨ b ≤ a

theorem ISize.lt_or_le (a b : ISize) : a < b ∨ b ≤ a

theorem Int8.le_or_lt (a b : Int8) : a ≤ b ∨ b < a

theorem Int16.le_or_lt (a b : Int16) : a ≤ b ∨ b < a

theorem Int32.le_or_lt (a b : Int32) : a ≤ b ∨ b < a

theorem Int64.le_or_lt (a b : Int64) : a ≤ b ∨ b < a

theorem ISize.le_or_lt (a b : ISize) : a ≤ b ∨ b < a

theorem Int8.le_of_eq {a b : Int8} : a = b → a ≤ b

theorem Int16.le_of_eq {a b : Int16} : a = b → a ≤ b

theorem Int32.le_of_eq {a b : Int32} : a = b → a ≤ b

theorem Int64.le_of_eq {a b : Int64} : a = b → a ≤ b

theorem ISize.le_of_eq {a b : ISize} : a = b → a ≤ b

theorem Int8.le_iff_lt_or_eq {a b : Int8} : a ≤ b ↔ a < b ∨ a = b

theorem Int16.le_iff_lt_or_eq {a b : Int16} : a ≤ b ↔ a < b ∨ a = b

theorem Int32.le_iff_lt_or_eq {a b : Int32} : a ≤ b ↔ a < b ∨ a = b

theorem Int64.le_iff_lt_or_eq {a b : Int64} : a ≤ b ↔ a < b ∨ a = b

theorem ISize.le_iff_lt_or_eq {a b : ISize} : a ≤ b ↔ a < b ∨ a = b

theorem Int8.lt_or_eq_of_le {a b : Int8} : a ≤ b → a < b ∨ a = b

theorem Int16.lt_or_eq_of_le {a b : Int16} : a ≤ b → a < b ∨ a = b

theorem Int32.lt_or_eq_of_le {a b : Int32} : a ≤ b → a < b ∨ a = b

theorem Int64.lt_or_eq_of_le {a b : Int64} : a ≤ b → a < b ∨ a = b

theorem ISize.lt_or_eq_of_le {a b : ISize} : a ≤ b → a < b ∨ a = b

theorem Int8.toInt_eq_toNatClampNeg {a : Int8} (ha : 0 ≤ a) : a.toInt = ↑a.toNatClampNeg

theorem Int16.toInt_eq_toNatClampNeg {a : Int16} (ha : 0 ≤ a) : a.toInt = ↑a.toNatClampNeg

theorem Int32.toInt_eq_toNatClampNeg {a : Int32} (ha : 0 ≤ a) : a.toInt = ↑a.toNatClampNeg

theorem Int64.toInt_eq_toNatClampNeg {a : Int64} (ha : 0 ≤ a) : a.toInt = ↑a.toNatClampNeg

theorem ISize.toInt_eq_toNatClampNeg {a : ISize} (ha : 0 ≤ a) : a.toInt = ↑a.toNatClampNeg

@[simp]

theorem UInt8.toInt8_add (a b : UInt8) : (a + b).toInt8 = a.toInt8 + b.toInt8

@[simp]

theorem UInt16.toInt16_add (a b : UInt16) : (a + b).toInt16 = a.toInt16 + b.toInt16

@[simp]

theorem UInt32.toInt32_add (a b : UInt32) : (a + b).toInt32 = a.toInt32 + b.toInt32

@[simp]

theorem UInt64.toInt64_add (a b : UInt64) : (a + b).toInt64 = a.toInt64 + b.toInt64

@[simp]

theorem USize.toISize_add (a b : USize) : (a + b).toISize = a.toISize + b.toISize

@[simp]

theorem UInt8.toInt8_neg (a : UInt8) : (-a).toInt8 = -a.toInt8

@[simp]

theorem UInt16.toInt16_neg (a : UInt16) : (-a).toInt16 = -a.toInt16

@[simp]

theorem UInt32.toInt32_neg (a : UInt32) : (-a).toInt32 = -a.toInt32

@[simp]

theorem UInt64.toInt64_neg (a : UInt64) : (-a).toInt64 = -a.toInt64

@[simp]

theorem USize.toISize_neg (a : USize) : (-a).toISize = -a.toISize

@[simp]

theorem UInt8.toInt8_sub (a b : UInt8) : (a - b).toInt8 = a.toInt8 - b.toInt8

@[simp]

theorem UInt16.toInt16_sub (a b : UInt16) : (a - b).toInt16 = a.toInt16 - b.toInt16

@[simp]

theorem UInt32.toInt32_sub (a b : UInt32) : (a - b).toInt32 = a.toInt32 - b.toInt32

@[simp]

theorem UInt64.toInt64_sub (a b : UInt64) : (a - b).toInt64 = a.toInt64 - b.toInt64

@[simp]

theorem USize.toISize_sub (a b : USize) : (a - b).toISize = a.toISize - b.toISize

@[simp]

theorem UInt8.toInt8_mul (a b : UInt8) : (a * b).toInt8 = a.toInt8 * b.toInt8

@[simp]

theorem UInt16.toInt16_mul (a b : UInt16) : (a * b).toInt16 = a.toInt16 * b.toInt16

@[simp]

theorem UInt32.toInt32_mul (a b : UInt32) : (a * b).toInt32 = a.toInt32 * b.toInt32

@[simp]

theorem UInt64.toInt64_mul (a b : UInt64) : (a * b).toInt64 = a.toInt64 * b.toInt64

@[simp]

theorem USize.toISize_mul (a b : USize) : (a * b).toISize = a.toISize * b.toISize

@[simp]

theorem Int8.toUInt8_add (a b : Int8) : (a + b).toUInt8 = a.toUInt8 + b.toUInt8

@[simp]

theorem Int16.toUInt16_add (a b : Int16) : (a + b).toUInt16 = a.toUInt16 + b.toUInt16

@[simp]

theorem Int32.toUInt32_add (a b : Int32) : (a + b).toUInt32 = a.toUInt32 + b.toUInt32

@[simp]

theorem Int64.toUInt64_add (a b : Int64) : (a + b).toUInt64 = a.toUInt64 + b.toUInt64

@[simp]

theorem ISize.toUSize_add (a b : ISize) : (a + b).toUSize = a.toUSize + b.toUSize

@[simp]

theorem Int8.toUInt8_neg (a : Int8) : (-a).toUInt8 = -a.toUInt8

@[simp]

theorem Int16.toUInt16_neg (a : Int16) : (-a).toUInt16 = -a.toUInt16

@[simp]

theorem Int32.toUInt32_neg (a : Int32) : (-a).toUInt32 = -a.toUInt32

@[simp]

theorem Int64.toUInt64_neg (a : Int64) : (-a).toUInt64 = -a.toUInt64

@[simp]

theorem ISize.toUSize_neg (a : ISize) : (-a).toUSize = -a.toUSize

@[simp]

theorem Int8.toUInt8_sub (a b : Int8) : (a - b).toUInt8 = a.toUInt8 - b.toUInt8

@[simp]

theorem Int16.toUInt16_sub (a b : Int16) : (a - b).toUInt16 = a.toUInt16 - b.toUInt16

@[simp]

theorem Int32.toUInt32_sub (a b : Int32) : (a - b).toUInt32 = a.toUInt32 - b.toUInt32

@[simp]

theorem Int64.toUInt64_sub (a b : Int64) : (a - b).toUInt64 = a.toUInt64 - b.toUInt64

@[simp]

theorem ISize.toUSize_sub (a b : ISize) : (a - b).toUSize = a.toUSize - b.toUSize

@[simp]

theorem Int8.toUInt8_mul (a b : Int8) : (a * b).toUInt8 = a.toUInt8 * b.toUInt8

@[simp]

theorem Int16.toUInt16_mul (a b : Int16) : (a * b).toUInt16 = a.toUInt16 * b.toUInt16

@[simp]

theorem Int32.toUInt32_mul (a b : Int32) : (a * b).toUInt32 = a.toUInt32 * b.toUInt32

@[simp]

theorem Int64.toUInt64_mul (a b : Int64) : (a * b).toUInt64 = a.toUInt64 * b.toUInt64

@[simp]

theorem ISize.toUSize_mul (a b : ISize) : (a * b).toUSize = a.toUSize * b.toUSize

theorem Int8.toNatClampNeg_le {a b : Int8} (hab : a ≤ b) : a.toNatClampNeg ≤ b.toNatClampNeg

theorem Int16.toNatClampNeg_le {a b : Int16} (hab : a ≤ b) : a.toNatClampNeg ≤ b.toNatClampNeg

theorem Int32.toNatClampNeg_le {a b : Int32} (hab : a ≤ b) : a.toNatClampNeg ≤ b.toNatClampNeg

theorem Int64.toNatClampNeg_le {a b : Int64} (hab : a ≤ b) : a.toNatClampNeg ≤ b.toNatClampNeg

theorem ISize.toNatClampNeg_le {a b : ISize} (hab : a ≤ b) : a.toNatClampNeg ≤ b.toNatClampNeg

theorem Int8.toUInt8_le {a b : Int8} (ha : 0 ≤ a) (hab : a ≤ b) : a.toUInt8 ≤ b.toUInt8

theorem Int16.toUInt16_le {a b : Int16} (ha : 0 ≤ a) (hab : a ≤ b) : a.toUInt16 ≤ b.toUInt16

theorem Int32.toUInt32_le {a b : Int32} (ha : 0 ≤ a) (hab : a ≤ b) : a.toUInt32 ≤ b.toUInt32

theorem Int64.toUInt64_le {a b : Int64} (ha : 0 ≤ a) (hab : a ≤ b) : a.toUInt64 ≤ b.toUInt64

theorem ISize.toUSize_le {a b : ISize} (ha : 0 ≤ a) (hab : a ≤ b) : a.toUSize ≤ b.toUSize

theorem Int8.zero_le_ofNat_of_lt {a : Nat} (ha : a < 2 ^ 7) : 0 ≤ ofNat a

theorem Int16.zero_le_ofNat_of_lt {a : Nat} (ha : a < 2 ^ 15) : 0 ≤ ofNat a

theorem Int32.zero_le_ofNat_of_lt {a : Nat} (ha : a < 2 ^ 31) : 0 ≤ ofNat a

theorem Int64.zero_le_ofNat_of_lt {a : Nat} (ha : a < 2 ^ 63) : 0 ≤ ofNat a

theorem ISize.zero_le_ofNat_of_lt {a : Nat} (ha : a < 2 ^ (System.Platform.numBits - 1)) : 0 ≤ ofNat a

theorem Int8.sub_nonneg_of_le {a b : Int8} (hb : 0 ≤ b) (hab : b ≤ a) : 0 ≤ a - b

theorem Int16.sub_nonneg_of_le {a b : Int16} (hb : 0 ≤ b) (hab : b ≤ a) : 0 ≤ a - b

theorem Int32.sub_nonneg_of_le {a b : Int32} (hb : 0 ≤ b) (hab : b ≤ a) : 0 ≤ a - b

theorem Int64.sub_nonneg_of_le {a b : Int64} (hb : 0 ≤ b) (hab : b ≤ a) : 0 ≤ a - b

theorem ISize.sub_nonneg_of_le {a b : ISize} (hb : 0 ≤ b) (hab : b ≤ a) : 0 ≤ a - b

theorem Int8.toNatClampNeg_sub_of_le {a b : Int8} (hb : 0 ≤ b) (hab : b ≤ a) : (a - b).toNatClampNeg = a.toNatClampNeg - b.toNatClampNeg

theorem Int16.toNatClampNeg_sub_of_le {a b : Int16} (hb : 0 ≤ b) (hab : b ≤ a) : (a - b).toNatClampNeg = a.toNatClampNeg - b.toNatClampNeg

theorem Int32.toNatClampNeg_sub_of_le {a b : Int32} (hb : 0 ≤ b) (hab : b ≤ a) : (a - b).toNatClampNeg = a.toNatClampNeg - b.toNatClampNeg

theorem Int64.toNatClampNeg_sub_of_le {a b : Int64} (hb : 0 ≤ b) (hab : b ≤ a) : (a - b).toNatClampNeg = a.toNatClampNeg - b.toNatClampNeg

theorem ISize.toNatClampNeg_sub_of_le {a b : ISize} (hb : 0 ≤ b) (hab : b ≤ a) : (a - b).toNatClampNeg = a.toNatClampNeg - b.toNatClampNeg

theorem Int8.toInt_sub_of_le (a b : Int8) (hb : 0 ≤ b) (h : b ≤ a) : (a - b).toInt = a.toInt - b.toInt

theorem Int16.toInt_sub_of_le (a b : Int16) (hb : 0 ≤ b) (h : b ≤ a) : (a - b).toInt = a.toInt - b.toInt

theorem Int32.toInt_sub_of_le (a b : Int32) (hb : 0 ≤ b) (h : b ≤ a) : (a - b).toInt = a.toInt - b.toInt

theorem Int64.toInt_sub_of_le (a b : Int64) (hb : 0 ≤ b) (h : b ≤ a) : (a - b).toInt = a.toInt - b.toInt

theorem ISize.toInt_sub_of_le (a b : ISize) (hb : 0 ≤ b) (h : b ≤ a) : (a - b).toInt = a.toInt - b.toInt

theorem Int8.sub_le {a b : Int8} (hb : 0 ≤ b) (hab : b ≤ a) : a - b ≤ a

theorem Int16.sub_le {a b : Int16} (hb : 0 ≤ b) (hab : b ≤ a) : a - b ≤ a

theorem Int32.sub_le {a b : Int32} (hb : 0 ≤ b) (hab : b ≤ a) : a - b ≤ a

theorem Int64.sub_le {a b : Int64} (hb : 0 ≤ b) (hab : b ≤ a) : a - b ≤ a

theorem ISize.sub_le {a b : ISize} (hb : 0 ≤ b) (hab : b ≤ a) : a - b ≤ a

theorem Int8.sub_lt {a b : Int8} (hb : 0 < b) (hab : b ≤ a) : a - b < a

theorem Int16.sub_lt {a b : Int16} (hb : 0 < b) (hab : b ≤ a) : a - b < a

theorem Int32.sub_lt {a b : Int32} (hb : 0 < b) (hab : b ≤ a) : a - b < a

theorem Int64.sub_lt {a b : Int64} (hb : 0 < b) (hab : b ≤ a) : a - b < a

theorem ISize.sub_lt {a b : ISize} (hb : 0 < b) (hab : b ≤ a) : a - b < a

theorem Int8.ne_of_lt {a b : Int8} : a < b → a ≠ b

theorem Int16.ne_of_lt {a b : Int16} : a < b → a ≠ b

theorem Int32.ne_of_lt {a b : Int32} : a < b → a ≠ b

theorem Int64.ne_of_lt {a b : Int64} : a < b → a ≠ b

theorem ISize.ne_of_lt {a b : ISize} : a < b → a ≠ b

@[simp]

theorem Int8.toInt_mod (a b : Int8) : (a % b).toInt = a.toInt.tmod b.toInt

@[simp]

theorem Int16.toInt_mod (a b : Int16) : (a % b).toInt = a.toInt.tmod b.toInt

@[simp]

theorem Int32.toInt_mod (a b : Int32) : (a % b).toInt = a.toInt.tmod b.toInt

@[simp]

theorem Int64.toInt_mod (a b : Int64) : (a % b).toInt = a.toInt.tmod b.toInt

@[simp]

theorem ISize.toInt_mod (a b : ISize) : (a % b).toInt = a.toInt.tmod b.toInt

@[simp]

theorem Int8.toInt16_mod (a b : Int8) : (a % b).toInt16 = a.toInt16 % b.toInt16

@[simp]

theorem Int8.toInt32_mod (a b : Int8) : (a % b).toInt32 = a.toInt32 % b.toInt32

@[simp]

theorem Int8.toInt64_mod (a b : Int8) : (a % b).toInt64 = a.toInt64 % b.toInt64

@[simp]

theorem Int8.toISize_mod (a b : Int8) : (a % b).toISize = a.toISize % b.toISize

@[simp]

theorem Int16.toInt32_mod (a b : Int16) : (a % b).toInt32 = a.toInt32 % b.toInt32

@[simp]

theorem Int16.toInt64_mod (a b : Int16) : (a % b).toInt64 = a.toInt64 % b.toInt64

@[simp]

theorem Int16.toISize_mod (a b : Int16) : (a % b).toISize = a.toISize % b.toISize

@[simp]

theorem Int32.toInt64_mod (a b : Int32) : (a % b).toInt64 = a.toInt64 % b.toInt64

@[simp]

theorem Int32.toISize_mod (a b : Int32) : (a % b).toISize = a.toISize % b.toISize

@[simp]

theorem ISize.toInt64_mod (a b : ISize) : (a % b).toInt64 = a.toInt64 % b.toInt64

theorem Int8.ofInt_tmod {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofInt (a.tmod b) = ofInt a % ofInt b

theorem Int16.ofInt_tmod {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofInt (a.tmod b) = ofInt a % ofInt b

theorem Int32.ofInt_tmod {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofInt (a.tmod b) = ofInt a % ofInt b

theorem Int64.ofInt_tmod {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofInt (a.tmod b) = ofInt a % ofInt b

theorem ISize.ofInt_tmod {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofInt (a.tmod b) = ofInt a % ofInt b

theorem Int8.ofInt_eq_ofIntLE_mod {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofInt (a.tmod b) = ofIntLE a ha₁ ha₂ % ofIntLE b hb₁ hb₂

theorem Int16.ofInt_eq_ofIntLE_mod {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofInt (a.tmod b) = ofIntLE a ha₁ ha₂ % ofIntLE b hb₁ hb₂

theorem Int32.ofInt_eq_ofIntLE_mod {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofInt (a.tmod b) = ofIntLE a ha₁ ha₂ % ofIntLE b hb₁ hb₂

theorem Int64.ofInt_eq_ofIntLE_mod {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofInt (a.tmod b) = ofIntLE a ha₁ ha₂ % ofIntLE b hb₁ hb₂

theorem ISize.ofInt_eq_ofIntLE_mod {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) : ofInt (a.tmod b) = ofIntLE a ha₁ ha₂ % ofIntLE b hb₁ hb₂

theorem Int8.ofNat_mod {a b : Nat} (ha : a < 2 ^ 7) (hb : b < 2 ^ 7) : ofNat (a % b) = ofNat a % ofNat b

theorem Int16.ofNat_mod {a b : Nat} (ha : a < 2 ^ 15) (hb : b < 2 ^ 15) : ofNat (a % b) = ofNat a % ofNat b

theorem Int32.ofNat_mod {a b : Nat} (ha : a < 2 ^ 31) (hb : b < 2 ^ 31) : ofNat (a % b) = ofNat a % ofNat b

theorem Int64.ofNat_mod {a b : Nat} (ha : a < 2 ^ 63) (hb : b < 2 ^ 63) : ofNat (a % b) = ofNat a % ofNat b

theorem ISize.ofNat_mod {a b : Nat} (ha : a < 2 ^ (System.Platform.numBits - 1)) (hb : b < 2 ^ (System.Platform.numBits - 1)) : ofNat (a % b) = ofNat a % ofNat b