proposition: Lemma zero_plus_alpha (alpha : Ord): zero + alpha = alpha.
proof: Proof. Proof with auto with schutte. pattern (plus zero); apply plus_elim ... intros f H0; assert (H1:ordering_function (fun o => o) ordinal ordinal). { (repeat split) ... - eauto with schutte. } rewrite ge_zero in H0. generalize (ordering_function_unicity H0 H1); destruct 1. apply H2; split. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles) ZornsLemma(CountableTypes)