proposition: Lemma plus_limit (alpha beta : Ord) : is_limit beta -> alpha + beta = |_| (image (members beta) (plus alpha)).
proof: Proof. intros H ; generalize (is_limit_sup_members H);intro e. generalize (@normal_plus_alpha alpha ); intro H2. pattern beta at 1;rewrite e; destruct H2 as [H0 [H1 [H2 H3]]]. rewrite <- H3;auto. - red;split. - case H. exists zero. red; auto with schutte. generalize (zero_le beta). intro H6; case (le_disj H6). + intro; subst beta; now destruct H4. + intros; now red. - apply countable_members; auto. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles) ZornsLemma(CountableTypes)