proposition: Lemma AP_plus_closed (alpha beta gamma : Ord): In AP alpha -> beta < alpha -> gamma < alpha -> beta + gamma < alpha.
proof: Proof. Proof with auto with schutte. intros H H0 H1; case H; intros H2 H3. generalize (@plus_mono_r beta gamma alpha); intro H4. replace alpha with (beta+alpha) ... Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)