obtain ⟨m, hm, hmp⟩ := hpn
case intro.succ
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
pn : ℕ
hpn : ∃ M, pn < M ∧ P M
⊢ ∃ M, pn + 1 < M ∧ P M
case intro.succ.intro.intro
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
pn m : ℕ
hm : pn < m
hmp : P m
⊢ ∃ M, pn + 1 < M ∧ P M