proposition: Lemma Min_less_Max_imp_ap : Min a b [<] Max a b -> a [#] b.
proof: Proof. intro H. elim (Min_less_imp _ _ _ H); clear H; intro H; elim (less_Max_imp _ _ _ H); intro H0. exfalso; exact (less_irreflexive _ _ H0). apply less_imp_ap; auto. apply Greater_imp_ap; auto. exfalso; exact (less_irreflexive _ _ H0). Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq