intros n hel
x y : ↑N0
A : Set ↑N0 := {x | plus (S y, x) = S (plus (x, y))}
hzmem : z ∈ A
⊢ ∀ n ∈ A, S n ∈ A
x y : ↑N0
A : Set ↑N0 := {x | plus (S y, x) = S (plus (x, y))}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ S n ∈ A