by_cases H : ∃ m < n, P m
case intro.ind
α : ℕ → Sort u
P : ℕ → Prop
n : ℕ
ih : ∀ m < n, P m → ∃ x, P x ∧ ∀ z < x, ¬P z
hn : P n
⊢ ∃ x, P x ∧ ∀ z < x, ¬P z
case pos
α : ℕ → Sort u
P : ℕ → Prop
n : ℕ
ih : ∀ m < n, P m → ∃ x, P x ∧ ∀ z < x, ¬P z
hn : P n
H : ∃ m < n, P m
⊢ ∃ x, P x ∧ ∀ z < x, ¬P z

case neg
α : ℕ → Sort u
P : ℕ → Prop
n : ℕ
ih : ∀ m < n, P m → ∃ x, P x ∧ ∀ z < x, ¬P z
hn : P n
H : ¬∃ m < n, P m
⊢ ∃ x, P x ∧ ∀ z < x, ¬P z