proposition: Lemma plus_mono_r_weak (alpha beta gamma : Ord) : beta <= gamma -> alpha + beta <= alpha + gamma.
proof: Proof. intros H; case (le_disj H). - intros; subst gamma; auto with schutte. - right; apply plus_mono_r;auto. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles) ZornsLemma(CountableTypes)