proposition: Lemma phi0_mono_R (alpha beta : Ord) : phi0 alpha < phi0 beta -> alpha < beta.
proof: Proof. pattern phi0; apply phi0_elim. intros;eapply ordering_function_monoR; eauto. all : split. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)