proposition: Lemma le_plus_l (alpha beta : Ord) : alpha <= alpha + beta.
proof: Proof. pattern alpha at 1; rewrite <- alpha_plus_zero;auto. pattern (plus alpha);apply plus_elim;auto. intros;eapply ordering_function_mono_weak;eauto with schutte. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles) ZornsLemma(CountableTypes)