R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
⊢ bit0 ↑n + 1 = bit1 ↑n
R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
⊢ ↑(bit1 n) = bit1 ↑n
rw [bit1, cast_add_one, cast_bit0]
no goals
R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
⊢ bit0 ↑n + 1 = bit1 ↑n
rfl