proposition: Lemma less_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_less. apply Max_less; apply inv_resp_less; assumption. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq