proposition: Lemma le_plus_r (alpha beta : Ord) : beta <= alpha + beta.
proof: Proof. pattern (plus alpha); apply plus_elim;auto. intros; eapply ordering_le. + apply H. + split. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles) ZornsLemma(CountableTypes)