Properties of the binary representation of integers

@[simp]

theorem PosNum.cast_one {α : Type u_1} [One α] [Add α] : ↑1 = 1

@[simp]

theorem PosNum.cast_one' {α : Type u_1} [One α] [Add α] : ↑PosNum.one = 1

@[simp]

theorem PosNum.cast_bit0 {α : Type u_1} [One α] [Add α] (n : PosNum) : ↑(PosNum.bit0 n) = bit0 ↑n

@[simp]

theorem PosNum.cast_bit1 {α : Type u_1} [One α] [Add α] (n : PosNum) : ↑(PosNum.bit1 n) = bit1 ↑n

@[simp]

theorem PosNum.cast_to_nat {α : Type u_1} [AddMonoidWithOne α] (n : PosNum) : ↑↑n = ↑n

theorem PosNum.to_nat_to_int (n : PosNum) : ↑↑n = ↑n

@[simp]

theorem PosNum.cast_to_int {α : Type u_1} [AddGroupWithOne α] (n : PosNum) : ↑↑n = ↑n

theorem PosNum.succ_to_nat (n : PosNum) : ↑(PosNum.succ n) = ↑n + 1

theorem PosNum.one_add (n : PosNum) : 1 + n = PosNum.succ n

theorem PosNum.add_one (n : PosNum) : n + 1 = PosNum.succ n

theorem PosNum.add_to_nat (m : PosNum) (n : PosNum) : ↑(m + n) = ↑m + ↑n

theorem PosNum.add_succ (m : PosNum) (n : PosNum) : m + PosNum.succ n = PosNum.succ (m + n)

theorem PosNum.bit0_of_bit0 (n : PosNum) : bit0 n = PosNum.bit0 n

theorem PosNum.bit1_of_bit1 (n : PosNum) : bit1 n = PosNum.bit1 n

theorem PosNum.mul_to_nat (m : PosNum) (n : PosNum) : ↑(m * n) = ↑m * ↑n

theorem PosNum.to_nat_pos (n : PosNum) : 0 < ↑n

theorem PosNum.cmp_to_nat_lemma {m : PosNum} {n : PosNum} : ↑m < ↑n → ↑(PosNum.bit1 m) < ↑(PosNum.bit0 n)

theorem PosNum.cmp_swap (m : PosNum) (n : PosNum) : Ordering.swap (PosNum.cmp m n) = PosNum.cmp n m

theorem PosNum.cmp_to_nat (m : PosNum) (n : PosNum) : Ordering.casesOn (PosNum.cmp m n) (↑m < ↑n) (m = n) (↑n < ↑m)

theorem PosNum.lt_to_nat {m : PosNum} {n : PosNum} : ↑m < ↑n ↔ m < n

theorem PosNum.le_to_nat {m : PosNum} {n : PosNum} : ↑m ≤ ↑n ↔ m ≤ n

theorem Num.add_zero (n : Num) : n + 0 = n

theorem Num.zero_add (n : Num) : 0 + n = n

theorem Num.add_one (n : Num) : n + 1 = Num.succ n

theorem Num.add_succ (m : Num) (n : Num) : m + Num.succ n = Num.succ (m + n)

theorem Num.bit0_of_bit0 (n : Num) : bit0 n = Num.bit0 n

theorem Num.bit1_of_bit1 (n : Num) : bit1 n = Num.bit1 n

@[simp]

theorem Num.ofNat'_zero : Num.ofNat' 0 = 0

theorem Num.ofNat'_bit (b : Bool) (n : ℕ) : Num.ofNat' (Nat.bit b n) = (bif b then Num.bit1 else Num.bit0) (Num.ofNat' n)

@[simp]

theorem Num.ofNat'_one : Num.ofNat' 1 = 1

theorem Num.bit1_succ (n : Num) : Num.succ (Num.bit1 n) = Num.bit0 (Num.succ n)

theorem Num.ofNat'_succ {n : ℕ} : Num.ofNat' (n + 1) = Num.ofNat' n + 1

@[simp]

theorem Num.add_ofNat' (m : ℕ) (n : ℕ) : Num.ofNat' (m + n) = Num.ofNat' m + Num.ofNat' n

@[simp]

theorem Num.cast_zero {α : Type u_1} [Zero α] [One α] [Add α] : ↑0 = 0

@[simp]

theorem Num.cast_zero' {α : Type u_1} [Zero α] [One α] [Add α] : ↑Num.zero = 0

@[simp]

theorem Num.cast_one {α : Type u_1} [Zero α] [One α] [Add α] : ↑1 = 1

@[simp]

theorem Num.cast_pos {α : Type u_1} [Zero α] [One α] [Add α] (n : PosNum) : ↑(Num.pos n) = ↑n

theorem Num.succ'_to_nat (n : Num) : ↑(Num.succ' n) = ↑n + 1

theorem Num.succ_to_nat (n : Num) : ↑(Num.succ n) = ↑n + 1

@[simp]

theorem Num.cast_to_nat {α : Type u_1} [AddMonoidWithOne α] (n : Num) : ↑↑n = ↑n

theorem Num.add_to_nat (m : Num) (n : Num) : ↑(m + n) = ↑m + ↑n

theorem Num.mul_to_nat (m : Num) (n : Num) : ↑(m * n) = ↑m * ↑n

theorem Num.cmp_to_nat (m : Num) (n : Num) : Ordering.casesOn (Num.cmp m n) (↑m < ↑n) (m = n) (↑n < ↑m)

theorem Num.lt_to_nat {m : Num} {n : Num} : ↑m < ↑n ↔ m < n

theorem Num.le_to_nat {m : Num} {n : Num} : ↑m ≤ ↑n ↔ m ≤ n

@[simp]

theorem PosNum.of_to_nat' (n : PosNum) : Num.ofNat' ↑n = Num.pos n

@[simp]

theorem Num.of_to_nat' (n : Num) : Num.ofNat' ↑n = n

theorem Num.toNat_injective : Function.Injective castNum

theorem Num.to_nat_inj {m : Num} {n : Num} : ↑m = ↑n ↔ m = n

def Num.transfer_rw : Lean.ParserDescr

This tactic tries to turn an (in)equality about Nums to one about Nats by rewriting.

example (n : Num) (m : Num) : n ≤ n + m := by
  transfer_rw
  exact Nat.le_add_right _ _

Equations

• Num.transfer_rw = Lean.ParserDescr.node `Num.transfer_rw 1024 (Lean.ParserDescr.nonReservedSymbol "transfer_rw" false)

def Num.transfer : Lean.ParserDescr

This tactic tries to prove (in)equalities about Nums by transferring them to the Nat world and then trying to call simp.

example (n : Num) (m : Num) : n ≤ n + m := by transfer

Equations

• Num.transfer = Lean.ParserDescr.node `Num.transfer 1024 (Lean.ParserDescr.nonReservedSymbol "transfer" false)

instance Num.addMonoid : AddMonoid Num

Equations

• Num.addMonoid = AddMonoid.mk Num.zero_add Num.add_zero nsmulRec

instance Num.addMonoidWithOne : AddMonoidWithOne Num

Equations

• Num.addMonoidWithOne = let src := Num.addMonoid; AddMonoidWithOne.mk

instance Num.commSemiring : CommSemiring Num

Equations

• Num.commSemiring = let src := Num.addMonoid; let src_1 := Num.addMonoidWithOne; CommSemiring.mk Num.commSemiring.proof_11

instance Num.orderedCancelAddCommMonoid : OrderedCancelAddCommMonoid Num

Equations

• Num.orderedCancelAddCommMonoid = OrderedCancelAddCommMonoid.mk Num.orderedCancelAddCommMonoid.proof_6

instance Num.linearOrderedSemiring : LinearOrderedSemiring Num

Equations

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

theorem Num.add_of_nat (m : ℕ) (n : ℕ) : ↑(m + n) = ↑m + ↑n

theorem Num.to_nat_to_int (n : Num) : ↑↑n = ↑n

@[simp]

theorem Num.cast_to_int {α : Type u_1} [AddGroupWithOne α] (n : Num) : ↑↑n = ↑n

theorem Num.to_of_nat (n : ℕ) : ↑↑n = n

@[simp]

theorem Num.of_nat_cast {α : Type u_1} [AddMonoidWithOne α] (n : ℕ) : ↑↑n = ↑n

theorem Num.of_nat_inj {m : ℕ} {n : ℕ} : ↑m = ↑n ↔ m = n

@[simp]

theorem Num.of_to_nat (n : Num) : ↑↑n = n

theorem Num.dvd_to_nat (m : Num) (n : Num) : ↑m ∣ ↑n ↔ m ∣ n

@[simp]

theorem PosNum.of_to_nat (n : PosNum) : ↑↑n = Num.pos n

theorem PosNum.to_nat_inj {m : PosNum} {n : PosNum} : ↑m = ↑n ↔ m = n

theorem PosNum.pred'_to_nat (n : PosNum) : ↑(PosNum.pred' n) = Nat.pred ↑n

@[simp]

theorem PosNum.pred'_succ' (n : Num) : PosNum.pred' (Num.succ' n) = n

@[simp]

theorem PosNum.succ'_pred' (n : PosNum) : Num.succ' (PosNum.pred' n) = n

instance PosNum.dvd : Dvd PosNum

Equations

• PosNum.dvd = { dvd := fun (m n : PosNum) => Num.pos m ∣ Num.pos n }

theorem PosNum.dvd_to_nat {m : PosNum} {n : PosNum} : ↑m ∣ ↑n ↔ m ∣ n

theorem PosNum.size_to_nat (n : PosNum) : ↑(PosNum.size n) = Nat.size ↑n

theorem PosNum.size_eq_natSize (n : PosNum) : ↑(PosNum.size n) = PosNum.natSize n

theorem PosNum.natSize_to_nat (n : PosNum) : PosNum.natSize n = Nat.size ↑n

theorem PosNum.natSize_pos (n : PosNum) : 0 < PosNum.natSize n

def PosNum.transfer_rw : Lean.ParserDescr

This tactic tries to turn an (in)equality about PosNums to one about Nats by rewriting.

example (n : PosNum) (m : PosNum) : n ≤ n + m := by
  transfer_rw
  exact Nat.le_add_right _ _

Equations

• PosNum.transfer_rw = Lean.ParserDescr.node `PosNum.transfer_rw 1024 (Lean.ParserDescr.nonReservedSymbol "transfer_rw" false)

def PosNum.transfer : Lean.ParserDescr

This tactic tries to prove (in)equalities about PosNums by transferring them to the Nat world and then trying to call simp.

example (n : PosNum) (m : PosNum) : n ≤ n + m := by transfer

Equations

• PosNum.transfer = Lean.ParserDescr.node `PosNum.transfer 1024 (Lean.ParserDescr.nonReservedSymbol "transfer" false)

instance PosNum.addCommSemigroup : AddCommSemigroup PosNum

Equations

• PosNum.addCommSemigroup = AddCommSemigroup.mk PosNum.addCommSemigroup.proof_2

instance PosNum.commMonoid : CommMonoid PosNum

Equations

• PosNum.commMonoid = CommMonoid.mk PosNum.commMonoid.proof_6

instance PosNum.distrib : Distrib PosNum

Equations

• PosNum.distrib = Distrib.mk PosNum.distrib.proof_1 PosNum.distrib.proof_2

instance PosNum.linearOrder : LinearOrder PosNum

Equations

• PosNum.linearOrder = LinearOrder.mk PosNum.linearOrder.proof_5 inferInstance inferInstance inferInstance

@[simp]

theorem PosNum.cast_to_num (n : PosNum) : ↑n = Num.pos n

@[simp]

theorem PosNum.bit_to_nat (b : Bool) (n : PosNum) : ↑(PosNum.bit b n) = Nat.bit b ↑n

@[simp]

theorem PosNum.cast_add {α : Type u_1} [AddMonoidWithOne α] (m : PosNum) (n : PosNum) : ↑(m + n) = ↑m + ↑n

@[simp]

theorem PosNum.cast_succ {α : Type u_1} [AddMonoidWithOne α] (n : PosNum) : ↑(PosNum.succ n) = ↑n + 1

@[simp]

theorem PosNum.cast_inj {α : Type u_1} [AddMonoidWithOne α] [CharZero α] {m : PosNum} {n : PosNum} : ↑m = ↑n ↔ m = n

@[simp]

theorem PosNum.one_le_cast {α : Type u_1} [LinearOrderedSemiring α] (n : PosNum) : 1 ≤ ↑n

@[simp]

theorem PosNum.cast_pos {α : Type u_1} [LinearOrderedSemiring α] (n : PosNum) : 0 < ↑n

@[simp]

theorem PosNum.cast_mul {α : Type u_1} [Semiring α] (m : PosNum) (n : PosNum) : ↑(m * n) = ↑m * ↑n

@[simp]

theorem PosNum.cmp_eq (m : PosNum) (n : PosNum) : PosNum.cmp m n = Ordering.eq ↔ m = n

@[simp]

theorem PosNum.cast_lt {α : Type u_1} [LinearOrderedSemiring α] {m : PosNum} {n : PosNum} : ↑m < ↑n ↔ m < n

@[simp]

theorem PosNum.cast_le {α : Type u_1} [LinearOrderedSemiring α] {m : PosNum} {n : PosNum} : ↑m ≤ ↑n ↔ m ≤ n

theorem Num.bit_to_nat (b : Bool) (n : Num) : ↑(Num.bit b n) = Nat.bit b ↑n

theorem Num.cast_succ' {α : Type u_1} [AddMonoidWithOne α] (n : Num) : ↑(Num.succ' n) = ↑n + 1

theorem Num.cast_succ {α : Type u_1} [AddMonoidWithOne α] (n : Num) : ↑(Num.succ n) = ↑n + 1

@[simp]

theorem Num.cast_add {α : Type u_1} [Semiring α] (m : Num) (n : Num) : ↑(m + n) = ↑m + ↑n

@[simp]

theorem Num.cast_bit0 {α : Type u_1} [Semiring α] (n : Num) : ↑(Num.bit0 n) = bit0 ↑n

@[simp]

theorem Num.cast_bit1 {α : Type u_1} [Semiring α] (n : Num) : ↑(Num.bit1 n) = bit1 ↑n

@[simp]

theorem Num.cast_mul {α : Type u_1} [Semiring α] (m : Num) (n : Num) : ↑(m * n) = ↑m * ↑n

theorem Num.size_to_nat (n : Num) : ↑(Num.size n) = Nat.size ↑n

theorem Num.size_eq_natSize (n : Num) : ↑(Num.size n) = Num.natSize n

theorem Num.natSize_to_nat (n : Num) : Num.natSize n = Nat.size ↑n

@[simp]

theorem Num.ofNat'_eq (n : ℕ) : Num.ofNat' n = ↑n

theorem Num.zneg_toZNum (n : Num) : -Num.toZNum n = Num.toZNumNeg n

theorem Num.zneg_toZNumNeg (n : Num) : -Num.toZNumNeg n = Num.toZNum n

theorem Num.toZNum_inj {m : Num} {n : Num} : Num.toZNum m = Num.toZNum n ↔ m = n

@[simp]

theorem Num.cast_toZNum {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] (n : Num) : ↑(Num.toZNum n) = ↑n

@[simp]

theorem Num.cast_toZNumNeg {α : Type u_1} [AddGroup α] [One α] (n : Num) : ↑(Num.toZNumNeg n) = -↑n

@[simp]

theorem Num.add_toZNum (m : Num) (n : Num) : Num.toZNum (m + n) = Num.toZNum m + Num.toZNum n

theorem PosNum.pred_to_nat {n : PosNum} (h : 1 < n) : ↑(PosNum.pred n) = Nat.pred ↑n

theorem PosNum.sub'_one (a : PosNum) : PosNum.sub' a 1 = Num.toZNum (PosNum.pred' a)

theorem PosNum.one_sub' (a : PosNum) : PosNum.sub' 1 a = Num.toZNumNeg (PosNum.pred' a)

theorem PosNum.lt_iff_cmp {m : PosNum} {n : PosNum} : m < n ↔ PosNum.cmp m n = Ordering.lt

theorem PosNum.le_iff_cmp {m : PosNum} {n : PosNum} : m ≤ n ↔ PosNum.cmp m n ≠ Ordering.gt

theorem Num.pred_to_nat (n : Num) : ↑(Num.pred n) = Nat.pred ↑n

theorem Num.ppred_to_nat (n : Num) : castNum <$> Num.ppred n = Nat.ppred ↑n

theorem Num.cmp_swap (m : Num) (n : Num) : Ordering.swap (Num.cmp m n) = Num.cmp n m

theorem Num.cmp_eq (m : Num) (n : Num) : Num.cmp m n = Ordering.eq ↔ m = n

@[simp]

theorem Num.cast_lt {α : Type u_1} [LinearOrderedSemiring α] {m : Num} {n : Num} : ↑m < ↑n ↔ m < n

@[simp]

theorem Num.cast_le {α : Type u_1} [LinearOrderedSemiring α] {m : Num} {n : Num} : ↑m ≤ ↑n ↔ m ≤ n

@[simp]

theorem Num.cast_inj {α : Type u_1} [LinearOrderedSemiring α] {m : Num} {n : Num} : ↑m = ↑n ↔ m = n

theorem Num.lt_iff_cmp {m : Num} {n : Num} : m < n ↔ Num.cmp m n = Ordering.lt

theorem Num.le_iff_cmp {m : Num} {n : Num} : m ≤ n ↔ Num.cmp m n ≠ Ordering.gt

theorem Num.castNum_eq_bitwise {f : Num → Num → Num} {g : Bool → Bool → Bool} (p : PosNum → PosNum → Num) (gff : g false false = false) (f00 : f 0 0 = 0) (f0n : ∀ (n : PosNum), f 0 (Num.pos n) = bif g false true then Num.pos n else 0) (fn0 : ∀ (n : PosNum), f (Num.pos n) 0 = bif g true false then Num.pos n else 0) (fnn : ∀ (m n : PosNum), f (Num.pos m) (Num.pos n) = p m n) (p11 : p 1 1 = bif g true true then 1 else 0) (p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = Num.bit (g true b) (bif g false true then Num.pos n else 0)) (pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = Num.bit (g a true) (bif g true false then Num.pos m else 0)) (pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = Num.bit (g a b) (p m n)) (m : Num) (n : Num) : ↑(f m n) = Nat.bitwise g ↑m ↑n

@[simp]

theorem Num.castNum_or (m : Num) (n : Num) : ↑(m ||| n) = ↑m ||| ↑n

@[simp]

theorem Num.castNum_and (m : Num) (n : Num) : ↑(m &&& n) = ↑m &&& ↑n

@[simp]

theorem Num.castNum_ldiff (m : Num) (n : Num) : ↑(Num.ldiff m n) = Nat.ldiff ↑m ↑n

@[simp]

theorem Num.castNum_xor (m : Num) (n : Num) : ↑(m ^^^ n) = ↑m ^^^ ↑n

@[simp]

theorem Num.castNum_shiftLeft (m : Num) (n : ℕ) : ↑(m <<< n) = ↑m <<< n

@[simp]

theorem Num.castNum_shiftRight (m : Num) (n : ℕ) : ↑(m >>> n) = ↑m >>> n

@[simp]

theorem Num.castNum_testBit (m : Num) (n : ℕ) : Num.testBit m n = Nat.testBit (↑m) n

@[simp]

theorem ZNum.cast_zero {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] : ↑0 = 0

@[simp]

theorem ZNum.cast_zero' {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] : ↑ZNum.zero = 0

@[simp]

theorem ZNum.cast_one {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] : ↑1 = 1

@[simp]

theorem ZNum.cast_pos {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] (n : PosNum) : ↑(ZNum.pos n) = ↑n

@[simp]

theorem ZNum.cast_neg {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] (n : PosNum) : ↑(ZNum.neg n) = -↑n

@[simp]

theorem ZNum.cast_zneg {α : Type u_1} [AddGroup α] [One α] (n : ZNum) : ↑(-n) = -↑n

theorem ZNum.neg_zero : -0 = 0

theorem ZNum.zneg_pos (n : PosNum) : -ZNum.pos n = ZNum.neg n

theorem ZNum.zneg_neg (n : PosNum) : -ZNum.neg n = ZNum.pos n

theorem ZNum.zneg_zneg (n : ZNum) : - -n = n

theorem ZNum.zneg_bit1 (n : ZNum) : -ZNum.bit1 n = ZNum.bitm1 (-n)

theorem ZNum.zneg_bitm1 (n : ZNum) : -ZNum.bitm1 n = ZNum.bit1 (-n)

theorem ZNum.zneg_succ (n : ZNum) : -ZNum.succ n = ZNum.pred (-n)

theorem ZNum.zneg_pred (n : ZNum) : -ZNum.pred n = ZNum.succ (-n)

@[simp]

theorem ZNum.abs_to_nat (n : ZNum) : ↑(ZNum.abs n) = Int.natAbs ↑n

@[simp]

theorem ZNum.abs_toZNum (n : Num) : ZNum.abs (Num.toZNum n) = n

@[simp]

theorem ZNum.cast_to_int {α : Type u_1} [AddGroupWithOne α] (n : ZNum) : ↑↑n = ↑n

theorem ZNum.bit0_of_bit0 (n : ZNum) : bit0 n = ZNum.bit0 n

theorem ZNum.bit1_of_bit1 (n : ZNum) : bit1 n = ZNum.bit1 n

@[simp]

theorem ZNum.cast_bit0 {α : Type u_1} [AddGroupWithOne α] (n : ZNum) : ↑(ZNum.bit0 n) = bit0 ↑n

@[simp]

theorem ZNum.cast_bit1 {α : Type u_1} [AddGroupWithOne α] (n : ZNum) : ↑(ZNum.bit1 n) = bit1 ↑n

@[simp]

theorem ZNum.cast_bitm1 {α : Type u_1} [AddGroupWithOne α] (n : ZNum) : ↑(ZNum.bitm1 n) = bit0 ↑n - 1

theorem ZNum.add_zero (n : ZNum) : n + 0 = n

theorem ZNum.zero_add (n : ZNum) : 0 + n = n

theorem ZNum.add_one (n : ZNum) : n + 1 = ZNum.succ n

theorem PosNum.cast_to_znum (n : PosNum) : ↑n = ZNum.pos n

theorem PosNum.cast_sub' {α : Type u_1} [AddGroupWithOne α] (m : PosNum) (n : PosNum) : ↑(PosNum.sub' m n) = ↑m - ↑n

theorem PosNum.to_nat_eq_succ_pred (n : PosNum) : ↑n = ↑(PosNum.pred' n) + 1

theorem PosNum.to_int_eq_succ_pred (n : PosNum) : ↑n = ↑↑(PosNum.pred' n) + 1

@[simp]

theorem Num.cast_sub' {α : Type u_1} [AddGroupWithOne α] (m : Num) (n : Num) : ↑(Num.sub' m n) = ↑m - ↑n

theorem Num.toZNum_succ (n : Num) : Num.toZNum (Num.succ n) = ZNum.succ (Num.toZNum n)

theorem Num.toZNumNeg_succ (n : Num) : Num.toZNumNeg (Num.succ n) = ZNum.pred (Num.toZNumNeg n)

@[simp]

theorem Num.pred_succ (n : ZNum) : ZNum.succ (ZNum.pred n) = n

theorem Num.succ_ofInt' (n : ℤ) : ZNum.ofInt' (n + 1) = ZNum.ofInt' n + 1

theorem Num.ofInt'_toZNum (n : ℕ) : Num.toZNum ↑n = ZNum.ofInt' ↑n

theorem Num.mem_ofZNum' {m : Num} {n : ZNum} : m ∈ Num.ofZNum' n ↔ n = Num.toZNum m

theorem Num.ofZNum'_toNat (n : ZNum) : castNum <$> Num.ofZNum' n = Int.toNat' ↑n

@[simp]

theorem Num.ofZNum_toNat (n : ZNum) : ↑(Num.ofZNum n) = Int.toNat ↑n

@[simp]

theorem Num.cast_ofZNum {α : Type u_1} [AddGroupWithOne α] (n : ZNum) : ↑(Num.ofZNum n) = ↑(Int.toNat ↑n)

@[simp]

theorem Num.sub_to_nat (m : Num) (n : Num) : ↑(m - n) = ↑m - ↑n

@[simp]

theorem ZNum.cast_add {α : Type u_1} [AddGroupWithOne α] (m : ZNum) (n : ZNum) : ↑(m + n) = ↑m + ↑n

@[simp]

theorem ZNum.cast_succ {α : Type u_1} [AddGroupWithOne α] (n : ZNum) : ↑(ZNum.succ n) = ↑n + 1

@[simp]

theorem ZNum.mul_to_int (m : ZNum) (n : ZNum) : ↑(m * n) = ↑m * ↑n

theorem ZNum.cast_mul {α : Type u_1} [Ring α] (m : ZNum) (n : ZNum) : ↑(m * n) = ↑m * ↑n

theorem ZNum.ofInt'_neg (n : ℤ) : ZNum.ofInt' (-n) = -ZNum.ofInt' n

theorem ZNum.of_to_int' (n : ZNum) : ZNum.ofInt' ↑n = n

theorem ZNum.to_int_inj {m : ZNum} {n : ZNum} : ↑m = ↑n ↔ m = n

theorem ZNum.cmp_to_int (m : ZNum) (n : ZNum) : Ordering.casesOn (ZNum.cmp m n) (↑m < ↑n) (m = n) (↑n < ↑m)

theorem ZNum.lt_to_int {m : ZNum} {n : ZNum} : ↑m < ↑n ↔ m < n

theorem ZNum.le_to_int {m : ZNum} {n : ZNum} : ↑m ≤ ↑n ↔ m ≤ n

@[simp]

theorem ZNum.cast_lt {α : Type u_1} [LinearOrderedRing α] {m : ZNum} {n : ZNum} : ↑m < ↑n ↔ m < n

@[simp]

theorem ZNum.cast_le {α : Type u_1} [LinearOrderedRing α] {m : ZNum} {n : ZNum} : ↑m ≤ ↑n ↔ m ≤ n

@[simp]

theorem ZNum.cast_inj {α : Type u_1} [LinearOrderedRing α] {m : ZNum} {n : ZNum} : ↑m = ↑n ↔ m = n

def ZNum.transfer_rw : Lean.ParserDescr

This tactic tries to turn an (in)equality about ZNums to one about Ints by rewriting.

example (n : ZNum) (m : ZNum) : n ≤ n + m * m := by
  transfer_rw
  exact le_add_of_nonneg_right (mul_self_nonneg _)

Equations

• ZNum.transfer_rw = Lean.ParserDescr.node `ZNum.transfer_rw 1024 (Lean.ParserDescr.nonReservedSymbol "transfer_rw" false)

def ZNum.transfer : Lean.ParserDescr

This tactic tries to prove (in)equalities about ZNums by transferring them to the Int world and then trying to call simp.

example (n : ZNum) (m : ZNum) : n ≤ n + m * m := by
  transfer
  exact mul_self_nonneg _

Equations

• ZNum.transfer = Lean.ParserDescr.node `ZNum.transfer 1024 (Lean.ParserDescr.nonReservedSymbol "transfer" false)

instance ZNum.linearOrder : LinearOrder ZNum

Equations

• ZNum.linearOrder = LinearOrder.mk ZNum.linearOrder.proof_5 ZNum.decidableLE instDecidableEqZNum ZNum.decidableLT

instance ZNum.addMonoid : AddMonoid ZNum

Equations

• ZNum.addMonoid = AddMonoid.mk ZNum.zero_add ZNum.add_zero nsmulRec

instance ZNum.addCommGroup : AddCommGroup ZNum

Equations

• ZNum.addCommGroup = let src := ZNum.addMonoid; AddCommGroup.mk ZNum.addCommGroup.proof_6

instance ZNum.addMonoidWithOne : AddMonoidWithOne ZNum

Equations

• ZNum.addMonoidWithOne = let src := ZNum.addMonoid; AddMonoidWithOne.mk

instance ZNum.linearOrderedCommRing : LinearOrderedCommRing ZNum

Equations

• ZNum.linearOrderedCommRing = let src := ZNum.linearOrder; let src_1 := ZNum.addCommGroup; let src_2 := ZNum.addMonoidWithOne; LinearOrderedCommRing.mk ZNum.mul_comm

@[simp]

theorem ZNum.cast_sub {α : Type u_1} [Ring α] (m : ZNum) (n : ZNum) : ↑(m - n) = ↑m - ↑n

theorem ZNum.neg_of_int (n : ℤ) : ↑(-n) = -↑n

@[simp]

theorem ZNum.ofInt'_eq (n : ℤ) : ZNum.ofInt' n = ↑n

@[simp]

theorem ZNum.of_nat_toZNum (n : ℕ) : Num.toZNum ↑n = ↑n

@[simp]

theorem ZNum.of_to_int (n : ZNum) : ↑↑n = n

theorem ZNum.to_of_int (n : ℤ) : ↑↑n = n

@[simp]

theorem ZNum.of_nat_toZNumNeg (n : ℕ) : Num.toZNumNeg ↑n = -↑n

@[simp]

theorem ZNum.of_int_cast {α : Type u_1} [AddGroupWithOne α] (n : ℤ) : ↑↑n = ↑n

@[simp]

theorem ZNum.of_nat_cast {α : Type u_1} [AddGroupWithOne α] (n : ℕ) : ↑↑n = ↑n

@[simp]

theorem ZNum.dvd_to_int (m : ZNum) (n : ZNum) : ↑m ∣ ↑n ↔ m ∣ n

theorem PosNum.divMod_to_nat_aux {n : PosNum} {d : PosNum} {q : Num} {r : Num} (h₁ : ↑r + ↑d * bit0 ↑q = ↑n) (h₂ : ↑r < 2 * ↑d) : ↑(PosNum.divModAux d q r).2 + ↑d * ↑(PosNum.divModAux d q r).1 = ↑n ∧ ↑(PosNum.divModAux d q r).2 < ↑d

theorem PosNum.divMod_to_nat (d : PosNum) (n : PosNum) : ↑n / ↑d = ↑(PosNum.divMod d n).1 ∧ ↑n % ↑d = ↑(PosNum.divMod d n).2

@[simp]

theorem PosNum.div'_to_nat (n : PosNum) (d : PosNum) : ↑(PosNum.div' n d) = ↑n / ↑d

@[simp]

theorem PosNum.mod'_to_nat (n : PosNum) (d : PosNum) : ↑(PosNum.mod' n d) = ↑n % ↑d

@[simp]

theorem Num.div_zero (n : Num) : n / 0 = 0

@[simp]

theorem Num.div_to_nat (n : Num) (d : Num) : ↑(n / d) = ↑n / ↑d

@[simp]

theorem Num.mod_zero (n : Num) : n % 0 = n

@[simp]

theorem Num.mod_to_nat (n : Num) (d : Num) : ↑(n % d) = ↑n % ↑d

theorem Num.gcd_to_nat_aux {n : ℕ} {a : Num} {b : Num} : a ≤ b → Num.natSize (a * b) ≤ n → ↑(Num.gcdAux n a b) = Nat.gcd ↑a ↑b

@[simp]

theorem Num.gcd_to_nat (a : Num) (b : Num) : ↑(Num.gcd a b) = Nat.gcd ↑a ↑b

theorem Num.dvd_iff_mod_eq_zero {m : Num} {n : Num} : m ∣ n ↔ n % m = 0

instance Num.decidableDvd : DecidableRel fun (x x_1 : Num) => x ∣ x_1

Equations

• Num.decidableDvd x✝ x = match x✝, x with | _a, _b => decidable_of_iff' (_b % _a = 0) (_ : _a ∣ _b ↔ _b % _a = 0)

instance PosNum.decidableDvd : DecidableRel fun (x x_1 : PosNum) => x ∣ x_1

Equations

• PosNum.decidableDvd x✝ x = match x✝, x with | _a, _b => Num.decidableDvd (Num.pos _a) (Num.pos _b)

@[simp]

theorem ZNum.div_zero (n : ZNum) : n / 0 = 0

@[simp]

theorem ZNum.div_to_int (n : ZNum) (d : ZNum) : ↑(n / d) = ↑n / ↑d

@[simp]

theorem ZNum.mod_to_int (n : ZNum) (d : ZNum) : ↑(n % d) = ↑n % ↑d

@[simp]

theorem ZNum.gcd_to_nat (a : ZNum) (b : ZNum) : ↑(ZNum.gcd a b) = Int.gcd ↑a ↑b

theorem ZNum.dvd_iff_mod_eq_zero {m : ZNum} {n : ZNum} : m ∣ n ↔ n % m = 0

instance ZNum.decidableDvd : DecidableRel fun (x x_1 : ZNum) => x ∣ x_1

Equations

• ZNum.decidableDvd x✝ x = match x✝, x with | _a, _b => decidable_of_iff' (_b % _a = 0) (_ : _a ∣ _b ↔ _b % _a = 0)

def Int.ofSnum : SNum → ℤ

Cast a SNum to the corresponding integer.

Equations

• Int.ofSnum = SNum.rec' (fun (a : Bool) => bif a then -1 else 0) fun (a : Bool) (_p : SNum) (IH : ℤ) => bif a then bit1 IH else bit0 IH

instance Int.snumCoe : Coe SNum ℤ

Equations

• Int.snumCoe = { coe := Int.ofSnum }

instance SNum.lt : LT SNum

Equations

• SNum.lt = { lt := fun (a b : SNum) => Int.ofSnum a < Int.ofSnum b }

instance SNum.le : LE SNum

Equations

• SNum.le = { le := fun (a b : SNum) => Int.ofSnum a ≤ Int.ofSnum b }