proposition: Lemma lt_phi0 (alpha : Ord): alpha < epsilon0 -> alpha < phi0 alpha.
proof: Proof. unfold epsilon0; intros H. specialize (@omega_limit_least_gt alpha omega_tower omega_tower_mono H); intro H0. destruct H0 as [i [H0 H1]]. destruct i as [|j]. - red in H0; simpl in H0; assert (H2 : alpha = zero). { specialize (lt_succ_le_2 _ H0); intro H3; apply le_alpha_zero; auto. } subst alpha; rewrite phi0_zero; auto. - assert (H2 : omega_tower j <= alpha). { tricho alpha (omega_tower j) H2. - specialize (H1 _ H2); assert False by (destruct H1; abstract lia); contradiction. - left; auto. - right;auto. } assert (omega_tower (S j) <= phi0 alpha). { simpl. now apply phi0_mono_weak. } apply lt_le_trans with (omega_tower (S j)); auto. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)