proposition: Lemma Min_is_lft_imp_leEq : forall x y : IR, Min x y [=] x -> x [<=] y.
proof: Proof. simpl; unfold MIN. intros. rstepl ( [--][--]x). rstepr ( [--][--]y). apply inv_resp_leEq. apply Max_is_rht_imp_leEq. astepl ( [--][--] (Max [--]y [--]x)). apply eq_transitive_unfolded with ( [--][--] (Max [--]x [--]y)). apply un_op_wd_unfolded; apply un_op_wd_unfolded; apply Max_comm. apply un_op_wd_unfolded; assumption. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq