proposition: Lemma AP_sup : In AP (|_| M).
proof: Proof. split. - apply supM_gt0. - intros ksi Hksi; destruct (@lt_sup_exists_lt M denM ksi Hksi) as [alpha [Malpha ksialpha]]. apply le_antisym. + rewrite alpha_plus_sup; auto. * apply sup_mono; auto. { apply R1 with ordinal (ge ksi); auto. - apply plus_ordering; eauto with schutte. - split. } { intros x H; destruct H as [beta [Mbeta ebeta]]. case (@lt_or_ge beta alpha);auto with schutte. - exists alpha; split;auto. subst x; case (OM Mbeta). intros H1 H2; right. apply lt_le_trans with (ksi + alpha). + apply plus_mono_r; eauto with schutte. + left. destruct (OM Malpha) as [H3 H4]; now apply H4. - exists beta; split; auto. left; subst x. case (OM Mbeta); intros H1 H2; apply H2. apply lt_le_trans with alpha;auto. } + apply le_plus_r;eauto with schutte. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)