proposition: Lemma is_limit_omega : is_limit omega.
proof: Proof. repeat split; auto with schutte. - intro H; absurd (F 1 < zero). + apply not_lt_zero;auto with schutte. + rewrite <- H; apply finite_lt_omega. - destruct 1 as [x Hx]. assert (x < omega). { rewrite Hx;auto with schutte. } destruct (lt_omega_finite H); subst x. assert (omega = F (S x0)) by (simpl; trivial). case ( @lt_irrefl omega);auto with schutte. pattern omega at 1;rewrite H0;auto with schutte. apply finite_lt_omega;auto with schutte. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)