no goals
α : Type ?u.173867
n : Num
⊢ 0 + succ n = succ (0 + n)
simp [zero_add]
α : Type ?u.173867
p : PosNum
⊢ pos (PosNum.succ p) = succ (pos p)
α : Type ?u.173867
p : PosNum
⊢ pos (p + 1) = succ (pos p + 0)
rw [PosNum.add_one, add_zero]
no goals
α : Type ?u.173867
p : PosNum
⊢ pos (PosNum.succ p) = succ (pos p)
rfl