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