proposition: Lemma minus_exists (alpha beta : Ord) : alpha <= beta -> exists gamma, alpha + gamma = beta.
proof: Proof. intro H; pattern (plus alpha); apply plus_elim;auto. intros f H2; case H2;intros H3 H4 H5 H6. case (H5 beta H). intros;exists x;auto. now destruct H0. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles) ZornsLemma(CountableTypes)