proposition: Lemma ksi_plus_beta : ksi + beta <= beta.
proof: Proof. unfold beta at 1; unfold omega_limit. rewrite alpha_plus_sup. - apply sup_least_upper_bound; eauto with schutte. + apply R1 with ordinal (ge ksi). * apply plus_ordering; auto. * apply seq_range_countable;auto. * intro; split. + intros y [z [H1 H2]]; subst y. destruct H1 as [x [_ H2]]; subst z; apply ksi_plus_seq_n'. - now exists (seq 0), 0. - eauto with schutte. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)