induction' n using Nat.strongRec with n ih
case intro
α : ℕ → Sort u
P : ℕ → Prop
n : ℕ
hn : P n
⊢ ∃ x, P x ∧ ∀ z < x, ¬P z
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