α : Type ?u.81357
n : PosNum
⊢ succ (bit0 n) = bit1 n
α : Type ?u.81357
n : PosNum
⊢ _root_.bit0 n + 1 = bit1 n
rw [add_one, bit0_of_bit0]
no goals
α : Type ?u.81357
n : PosNum
⊢ succ (bit0 n) = bit1 n
rfl