proposition: Lemma normal_plus_alpha (alpha : Ord) : normal (plus alpha) (ge alpha).
proof: Proof. unfold plus;pattern (ord (ge alpha)). unfold ord, some;apply epsilon_ind. - rewrite ge_o_segment; trivial. + exists (plus alpha);apply (plus_ordering alpha); auto. - intros a H0; rewrite ge_o_segment in H0; trivial. split; trivial. apply Th_13_5_2; trivial. + intros M H1 H2 H3; destruct H2; apply le_trans with x;auto. * specialize (H1 _ H); apply H1. * apply sup_upper_bound;auto. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles) ZornsLemma(CountableTypes)