apply generic_recursor
⊢ ∀ (a b : ↑N0), plus (a, b) = plus (b, a)
case hz

⊢ ∀ (b : ↑N0), plus (z, b) = plus (b, z)

case hs

⊢ ∀ (n : ↑N0), (∀ (b : ↑N0), plus (n, b) = plus (b, n)) → ∀ (b : ↑N0), plus (S n, b) = plus (b, S n)