rewrite-+-comm : (x y : ℕ) → x + y ≡ y + x
rewrite-+-comm zero y rewrite (+zero {y}) = refl
rewrite-+-comm (suc x) y = ?