+-comm : (x y : !$\mathbb{N}$!) !$\rightarrow$! x + y !$\equiv$! y + x
+-comm zero y rewrite (+zero {y}) = refl
+-comm (suc x) y = let open !$\equiv$!-Reasoning in
  begin
  ?0 !$\equiv$!!$\langle$! ?1 !$\rangle$!
  ?2 !$\blacksquare$!

-- ?0 : !$\mathbb{N}$! {(suc x) + y}
-- ?1 : suc x + y !$\equiv$! y + suc x
-- ?2 : !$\mathbb{N}$!