apply generic_recursor
⊢ ∀ (x y : ↑N0), plus (S y, x) = S (plus (x, y))
case hz

⊢ ∀ (y : ↑N0), plus (S y, z) = S (plus (z, y))

case hs

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