proposition: Lemma plus_ordering (alpha : Ord) : ordering_function (plus alpha) ordinal (ge alpha).
proof: Proof. unfold plus; generalize (@ord_ok (ge alpha)); rewrite ge_o_segment;auto. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles) ZornsLemma(CountableTypes)