proposition: Lemma equiv_imp_eq_max : forall x x' m, (forall y, x [<=] y -> x' [<=] y -> m [<=] y) -> (forall y, m [<=] y -> x [<=] y) -> (forall y, m [<=] y -> x' [<=] y) -> Max x x' [=] m.
proof: Proof. intros. apply not_ap_imp_eq. intros X. destruct (ap_imp_less _ _ _ X) as [X0|X0]. apply (less_irreflexive_unfolded _ (Max x x')). apply less_leEq_trans with m. assumption. apply H. apply lft_leEq_Max. apply rht_leEq_Max. case (less_Max_imp _ _ _ X0). change (Not (m[<]x)). rewrite <- (leEq_def). apply H0. apply leEq_reflexive. change (Not (m[<]x')). rewrite <- (leEq_def). apply H1. apply leEq_reflexive. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq