This version of + sucks

ThisSucks.agda

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat using (Nat; suc; zero)

cong : (f : Nat → Nat) → ∀ {a b} → a ≡ b → f a ≡ f b
cong f refl = refl
trans : ∀ {a b c : Nat} → a ≡ b → b ≡ c → a ≡ c
trans refl p = p
sym : ∀ {a b : Nat} → a ≡ b → b ≡ a
sym refl = refl

_+_ : Nat → Nat → Nat
a + zero = a
a + suc b = suc (b + a)

+-comm : ∀ a b → a + b ≡ b + a
+-suc : ∀ a b → suc a + b ≡ suc (b + a)
+-zero : ∀ a → zero + a ≡ a
+-comm zero b = +-zero b
+-comm (suc a) b = trans (+-suc a b) (cong suc (+-comm b a))
+-zero zero = refl
+-zero (suc a) = refl
+-suc a zero = cong suc (sym (+-zero a))
+-suc a (suc b) = cong suc (sym (+-suc b a))