rewrite-+-comm : (x y : !$\mathbb{N}$!) !$\rightarrow$! x + y !$\equiv$! y + x
rewrite-+-comm zero y rewrite (+zero {y}) = refl
rewrite-+-comm (suc x) y = ?