proposition: Lemma phi0_mono (alpha beta : Ord) : alpha < beta -> phi0 alpha < phi0 beta.
proof: Proof. intro H; pattern phi0; apply phi0_elim. intros;eapply ordering_function_mono;eauto with schutte. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)