α : Type ?u.80889
p : PosNum
⊢ bit0 (succ (bit0 p)) = bit0 (bit1 p)
α : Type ?u.80889
p : PosNum
⊢ bit0 (succ (_root_.bit0 p)) = bit0 (bit1 p)
rw [bit0_of_bit0 p]
no goals
α : Type ?u.80889
p : PosNum
⊢ bit0 (succ (bit0 p)) = bit0 (bit1 p)
rfl