proposition: Lemma Min_leEq_Max' : forall z : IR, Min a z [<=] Max b z.
proof: Proof. intros; apply leEq_transitive with z. apply Min_leEq_rht. apply rht_leEq_Max. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq