proposition: Lemma omega_limit_least (s : nat -> Ord) : seq_mono s -> forall y : Ord, (forall i, s i < y) -> omega_limit s <= y.
proof: Proof. intros H y H1. unfold omega_limit;apply sup_least_upper_bound;auto with schutte. intro y0; destruct 1 as [x [_ e]]; subst y0;auto. right; auto. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)