α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
⊢ ↑(ZNum.bitm1 (- -n)) = _root_.bit0 ↑n - 1
α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
⊢ ↑(ZNum.bitm1 n) = _root_.bit0 ↑n - 1
conv =>
  lhs
  rw [← zneg_zneg n]
α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
⊢ -_root_.bit1 ↑(-n) = _root_.bit0 ↑n - 1
α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
⊢ ↑(ZNum.bitm1 (- -n)) = _root_.bit0 ↑n - 1
rw [← zneg_bit1, cast_zneg, cast_bit1]
α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
this : ↑(-1 + ↑n + ↑n) = ↑(↑n + ↑n + -1)
⊢ -_root_.bit1 ↑(-n) = _root_.bit0 ↑n - 1
α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
⊢ -_root_.bit1 ↑(-n) = _root_.bit0 ↑n - 1
have : ((-1 + n + n : ℤ) : α) = (n + n + -1 : ℤ) := by simp [add_comm, add_left_comm]
no goals
α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
this : ↑(-1 + ↑n + ↑n) = ↑(↑n + ↑n + -1)
⊢ -_root_.bit1 ↑(-n) = _root_.bit0 ↑n - 1
simpa [_root_.bit1, _root_.bit0, sub_eq_add_neg] using this
no goals
α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
⊢ ↑(-1 + ↑n + ↑n) = ↑(↑n + ↑n + -1)
simp [add_comm, add_left_comm]