proposition: Lemma lt_omega_finite (alpha : Ord) : alpha < omega -> exists i:nat, alpha = i.
proof: Proof. intro H0; unfold omega_limit in H0. generalize (lt_sup_exists_leq (X:=(seq_range finite)) ). intros; assert (Countable (seq_range finite)) by apply seq_range_countable. generalize (H H1);clear H;intros. generalize (H _ H0);clear H;intros. destruct H as [x [H2 H3]]. destruct H2 as [x0 [_ e]]. subst x. destruct (le_disj H3). - exists x0; auto. - destruct (finite_lt_inv x0 H);auto. exists x; tauto. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)