proposition: Lemma omega_limit_least_gt (alpha : Ord) (s : nat -> Ord) (Hmono : forall i, s i < s (S i)) (H : alpha < omega_limit s) : exists i, least_member Peano.lt (fun j => alpha < s j) i.
proof: Proof. destruct (lt_omega_limit_lt_exists_lt s Hmono H ) as [i Hi]. destruct (well_order (fun i => alpha < s i) i) as [x Hx]; trivial. now exists x. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)