proposition: Lemma lt_omega_limit_lt_exists_lt (alpha : Ord) (s : nat -> Ord) : (forall i, s i < s (S i)) -> alpha < omega_limit s -> exists j, alpha < s j.
proof: Proof. intros H H0; unfold omega_limit in H0. assert (exists y, In (seq_range s) y /\ alpha < y). apply lt_sup_exists_lt; auto with schutte. destruct H1 as [y [[j [_ Hj]] H'y]]; subst y; now exists j. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)