proposition: Lemma lt_omega_limit (s : nat -> Ord) : seq_mono s -> forall i, s i < omega_limit s.
proof: Proof. unfold omega_limit;intros. apply lt_le_trans with (s (S i)). - eapply H; auto. - apply sup_upper_bound;auto with schutte. exists (S i);split;auto. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)