proposition: Lemma plus_assoc1 (gamma : Ord) : alpha + beta <= alpha + (beta + gamma) .
proof: Proof. intros;apply plus_mono_r_weak;auto. - apply le_plus_l; auto. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles) ZornsLemma(CountableTypes)