proposition: Lemma Min3_leEq_Max3 : forall c : IR, Min (Min a b) c [<=] Max (Max a b) c.
proof: Proof. intros; eapply leEq_transitive. apply Min_leEq_rht. apply rht_leEq_Max. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq