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