proposition: Remark of_g : ordering_function g_alpha_beta ordinal (ge (alpha+beta)).
proof: Proof. repeat split. - intros;red; red; unfold g_alpha_beta; now apply plus_assoc1. - intros b H; case (plus_assoc2 H). intros x H'x; exists x. unfold g_alpha_beta;split. split. symmetry; assumption. - unfold g_alpha_beta;intros. + apply plus_mono_r;auto with schutte. apply plus_mono_r;auto with schutte. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles) ZornsLemma(CountableTypes)