proposition: Lemma equiv_imp_eq_min : forall x x' m, (forall y, y [<=] x -> y [<=] x' -> y [<=] m) -> (forall y, y [<=] m -> y [<=] x) -> (forall y, y [<=] m -> y [<=] x') -> Min x x' [=] m.
proof: Proof. intros x x' m X X0 X1. simpl; unfold MIN. astepr ( [--][--]m). apply un_op_wd_unfolded. apply equiv_imp_eq_max. intros. rstepr ( [--][--]y). apply inv_resp_leEq. apply X. rstepr ( [--][--]x). apply inv_resp_leEq. assumption. rstepr ( [--][--]x'). apply inv_resp_leEq. assumption. intros. rstepr ( [--][--]y). apply inv_resp_leEq. apply X0. rstepr ( [--][--]m). apply inv_resp_leEq. assumption. intros. rstepr ( [--][--]y). apply inv_resp_leEq. apply X1. rstepr ( [--][--]m). apply inv_resp_leEq. assumption. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq