have hzmem : z ∈ A := by
  simp only [Set.mem_setOf_eq]
  rw [zplus, zero_plus_x_eq_eq]
x y : ↑N0
A : Set ↑N0 := {x | plus (S y, x) = S (plus (x, y))}
⊢ plus (S y, x) = S (plus (x, y))
x y : ↑N0
A : Set ↑N0 := {x | plus (S y, x) = S (plus (x, y))}
hzmem : z ∈ A
⊢ plus (S y, x) = S (plus (x, y))