proposition: Lemma phi0_positive (alpha : Ord): zero < phi0 alpha.
proof: Proof. intros; apply lt_le_trans with (phi0 zero). rewrite phi0_zero; eauto with schutte arith. pattern phi0 ; apply phi0_elim. intros; eapply ordering_function_mono_weak; eauto with schutte. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)