proposition: Lemma finite_lt_omega (i : nat) : i < omega.
proof: Proof. intros; apply lt_omega_limit; auto with schutte. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)