proposition: Lemma Max_comm : forall x y : IR, Max x y [=] Max y x.
proof: Proof. cut (forall x y : IR, Max x y [<=] Max y x). intros. apply leEq_imp_eq. apply H. apply H. intros. apply Max_leEq. apply rht_leEq_Max. apply lft_leEq_Max. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq