proposition: Lemma Min_leEq_rht : forall x y : IR, Min x y [<=] y.
proof: Proof. intros. simpl; unfold MIN. rstepr ( [--][--]y). apply inv_resp_leEq. apply rht_leEq_Max. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq