proposition: Lemma leEq_Min : forall x y z : IR, z [<=] x -> z [<=] y -> z [<=] Min x y.
proof: Proof. intros. simpl; unfold MIN. rstepl ( [--][--]z). apply inv_resp_leEq. apply Max_leEq; apply inv_resp_leEq; assumption. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq