proposition: Lemma alpha_plus_zero (alpha: Ord): alpha + zero = alpha.
proof: Proof. pattern (plus alpha); apply plus_elim;eauto. intros f H0 ; case (ordering_function_least_least H0). intros H1 H3; case (H3 alpha);auto. - red;red; auto with schutte. - intro H4; case H1. + symmetry;tauto. + intro; case (@lt_irrefl alpha);auto. apply lt_trans with (f zero);auto. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles) ZornsLemma(CountableTypes)