proposition: Lemma of_u : fun_equiv f_alpha_beta g_alpha_beta ordinal ordinal.
proof: Proof. eapply ordering_function_unicity. - unfold f_alpha_beta; apply plus_ordering. - apply of_g. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles) ZornsLemma(CountableTypes)