proposition: Lemma Max_is_rht_imp_leEq : forall x y : IR, Max x y [=] y -> x [<=] y.
proof: Proof. intros. rewrite -> leEq_def in |- *. intro H0. generalize (less_leEq _ _ _ H0); intro H1. generalize (leEq_imp_Max_is_rht _ _ H1); intro. cut (y [=] x). intro. elim (less_irreflexive_unfolded _ x). astepl y. assumption. astepl (Max x y). astepr (Max y x). apply Max_comm. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq