proposition: Lemma omega_eqn : omega = phi0 1.
proof: Proof. destruct (AP_to_phi0 (AP_omega)) as [beta Hbeta]; rewrite Hbeta; tricho beta (F 1) H. - destruct (finite_lt_inv 1 H ) as [i [H0 H1]]. inversion H0. + subst i beta; simpl in Hbeta; rewrite phi0_zero in Hbeta. specialize (finite_lt_omega 1); intro H1; rewrite Hbeta in H1. destruct (lt_irrefl H1). + inversion H3. - now subst. - specialize (phi0_mono H); intro H0; rewrite <- Hbeta in H0. specialize (lt_omega_finite H0);intros [i Hi]. specialize (@is_limit_phi0 (F 1)); intro H2. rewrite Hi in H2; destruct (finite_not_limit i). apply H2, lt_succ. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)