proposition: Lemma leEq_imp_Max_is_rht : forall x y : IR, x [<=] y -> Max x y [=] y.
proof: Proof. intros. apply leEq_imp_eq. apply Max_leEq. assumption. apply leEq_reflexive. apply rht_leEq_Max. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq