induction' N with pn hpn
case intro
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
N : ℕ
⊢ ∃ M, N < M ∧ P M
case intro.zero
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
⊢ ∃ M, 0 < M ∧ P M

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