obtain (hlt : pn + 1 < m) |  (hlte : m ≤ pn + 1) := lt_or_ge (pn + 1) 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
case intro.succ.intro.intro.inl
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
pn m : ℕ
hm : pn < m
hmp : P m
hlt : pn + 1 < m
⊢ ∃ M, pn + 1 < M ∧ P M

case intro.succ.intro.intro.inr
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
pn m : ℕ
hm : pn < m
hmp : P m
hlte : m ≤ pn + 1
⊢ ∃ M, pn + 1 < M ∧ P M