have hind : (∀ n : N0, n ∈ A → (S n) ∈ A) := by
  intros n hel
  simp only [Set.mem_setOf_eq]
  simp only [Set.mem_setOf_eq] at hel
  rw [splus, hel, succ_plus_eq_succ_plus]
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))
x y : ↑N0
A : Set ↑N0 := {x | plus (S y, x) = S (plus (x, y))}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
⊢ plus (S y, x) = S (plus (x, y))