proposition: Lemma Min_less_imp : forall x y z : IR, Min x y [<] z -> x [<] z or y [<] z.
proof: Proof. simpl; unfold MIN. intros. cut ( [--]z [<] [--]x or [--]z [<] [--]y). intros H0. elim H0; intro. left. apply inv_cancel_less; assumption. right. apply inv_cancel_less; assumption. apply less_Max_imp. apply inv_cancel_less. apply less_wdr with z. assumption. algebra. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq