α : Type u_1
inst✝ : AddGroupWithOne α
a : PosNum
⊢ ↑(↑a - 1) = ↑a - ↑1
α : Type u_1
inst✝ : AddGroupWithOne α
a : PosNum
⊢ ↑(sub' a 1) = ↑a - ↑1
rw [sub'_one, Num.cast_toZNum, ← Num.cast_to_nat, pred'_to_nat, ← Nat.sub_one]
no goals
α : Type u_1
inst✝ : AddGroupWithOne α
a : PosNum
⊢ ↑(↑a - 1) = ↑a - ↑1
simp [PosNum.cast_pos]
α : Type u_1
inst✝ : AddGroupWithOne α
b : PosNum
⊢ ↑(↑b - 1) = ↑b - ↑1
α : Type u_1
inst✝ : AddGroupWithOne α
b : PosNum
⊢ ↑(sub' 1 b) = ↑1 - ↑b
rw [one_sub', Num.cast_toZNumNeg, ← neg_sub, neg_inj, ← Num.cast_to_nat, pred'_to_nat,
    ← Nat.sub_one]
no goals
α : Type u_1
inst✝ : AddGroupWithOne α
b : PosNum
⊢ ↑(↑b - 1) = ↑b - ↑1
simp [PosNum.cast_pos]
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ _root_.bit0 (↑a - ↑b) = ↑(bit0 a) - ↑(bit0 b)
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(sub' (bit0 a) (bit0 b)) = ↑(bit0 a) - ↑(bit0 b)
rw [sub', ZNum.cast_bit0, cast_sub' a b]
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
this : ↑(↑a + -↑b + (↑a + -↑b)) = ↑a + ↑a + (-↑b + -↑b)
⊢ _root_.bit0 (↑a - ↑b) = ↑(bit0 a) - ↑(bit0 b)
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ _root_.bit0 (↑a - ↑b) = ↑(bit0 a) - ↑(bit0 b)
have : ((a + -b + (a + -b) : ℤ) : α) = a + a + (-b + -b) := by simp [add_left_comm]
no goals
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
this : ↑(↑a + -↑b + (↑a + -↑b)) = ↑a + ↑a + (-↑b + -↑b)
⊢ _root_.bit0 (↑a - ↑b) = ↑(bit0 a) - ↑(bit0 b)
simpa [_root_.bit0, sub_eq_add_neg] using this
no goals
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(↑a + -↑b + (↑a + -↑b)) = ↑a + ↑a + (-↑b + -↑b)
simp [add_left_comm]
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ _root_.bit0 (↑a - ↑b) - 1 = ↑(bit0 a) - ↑(bit1 b)
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(sub' (bit0 a) (bit1 b)) = ↑(bit0 a) - ↑(bit1 b)
rw [sub', ZNum.cast_bitm1, cast_sub' a b]
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
this : ↑(-↑b + (↑a + (-↑b + -1))) = ↑(↑a + -1 + (-↑b + -↑b))
⊢ _root_.bit0 (↑a - ↑b) - 1 = ↑(bit0 a) - ↑(bit1 b)
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ _root_.bit0 (↑a - ↑b) - 1 = ↑(bit0 a) - ↑(bit1 b)
have : ((-b + (a + (-b + -1)) : ℤ) : α) = (a + -1 + (-b + -b) : ℤ) := by
  simp [add_comm, add_left_comm]
no goals
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
this : ↑(-↑b + (↑a + (-↑b + -1))) = ↑(↑a + -1 + (-↑b + -↑b))
⊢ _root_.bit0 (↑a - ↑b) - 1 = ↑(bit0 a) - ↑(bit1 b)
simpa [_root_.bit1, _root_.bit0, sub_eq_add_neg] using this
no goals
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(-↑b + (↑a + (-↑b + -1))) = ↑(↑a + -1 + (-↑b + -↑b))
simp [add_comm, add_left_comm]
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ _root_.bit1 (↑a - ↑b) = ↑(bit1 a) - ↑(bit0 b)
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(sub' (bit1 a) (bit0 b)) = ↑(bit1 a) - ↑(bit0 b)
rw [sub', ZNum.cast_bit1, cast_sub' a b]
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
this : ↑(-↑b + (↑a + (-↑b + 1))) = ↑(↑a + 1 + (-↑b + -↑b))
⊢ _root_.bit1 (↑a - ↑b) = ↑(bit1 a) - ↑(bit0 b)
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ _root_.bit1 (↑a - ↑b) = ↑(bit1 a) - ↑(bit0 b)
have : ((-b + (a + (-b + 1)) : ℤ) : α) = (a + 1 + (-b + -b) : ℤ) := by
  simp [add_comm, add_left_comm]
no goals
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
this : ↑(-↑b + (↑a + (-↑b + 1))) = ↑(↑a + 1 + (-↑b + -↑b))
⊢ _root_.bit1 (↑a - ↑b) = ↑(bit1 a) - ↑(bit0 b)
simpa [_root_.bit1, _root_.bit0, sub_eq_add_neg] using this
no goals
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(-↑b + (↑a + (-↑b + 1))) = ↑(↑a + 1 + (-↑b + -↑b))
simp [add_comm, add_left_comm]
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ _root_.bit0 (↑a - ↑b) = ↑(bit1 a) - ↑(bit1 b)
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(sub' (bit1 a) (bit1 b)) = ↑(bit1 a) - ↑(bit1 b)
rw [sub', ZNum.cast_bit0, cast_sub' a b]
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
this : ↑(-↑b + (↑a + -↑b)) = ↑a + (-↑b + -↑b)
⊢ _root_.bit0 (↑a - ↑b) = ↑(bit1 a) - ↑(bit1 b)
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ _root_.bit0 (↑a - ↑b) = ↑(bit1 a) - ↑(bit1 b)
have : ((-b + (a + -b) : ℤ) : α) = a + (-b + -b) := by simp [add_left_comm]
no goals
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
this : ↑(-↑b + (↑a + -↑b)) = ↑a + (-↑b + -↑b)
⊢ _root_.bit0 (↑a - ↑b) = ↑(bit1 a) - ↑(bit1 b)
simpa [_root_.bit1, _root_.bit0, sub_eq_add_neg] using this
no goals
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(-↑b + (↑a + -↑b)) = ↑a + (-↑b + -↑b)
simp [add_left_comm]