have heq := p3 A ⟨hzmem, hind⟩
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
⊢ ∃ m, n = S m
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : Subtype.val '' A = N0
⊢ ∃ m, n = S m