α : Type u_1
inst✝ : Semiring α
n : Num
⊢ _root_.bit0 ↑n + ↑1 = _root_.bit1 ↑n
α : Type u_1
inst✝ : Semiring α
n : Num
⊢ ↑(Num.bit1 n) = _root_.bit1 ↑n
rw [← bit1_of_bit1, _root_.bit1, bit0_of_bit0, cast_add, cast_bit0]
no goals
α : Type u_1
inst✝ : Semiring α
n : Num
⊢ _root_.bit0 ↑n + ↑1 = _root_.bit1 ↑n
rfl