f : Ordinal → Ordinal
a b : Ordinal
⊢ a < (fun a => sup fun n => (f^[n]) a) b ↔ ∃ n, a < (f^[n]) b
f : Ordinal → Ordinal
a b : Ordinal
⊢ a < nfp f b ↔ ∃ n, a < (f^[n]) b
rw [← sup_iterate_eq_nfp]
no goals
f : Ordinal → Ordinal
a b : Ordinal
⊢ a < (fun a => sup fun n => (f^[n]) a) b ↔ ∃ n, a < (f^[n]) b
exact lt_sup