proposition: Lemma less_Max_imp : forall x y z : IR, z [<] Max x y -> z [<] x or z [<] y.
proof: Proof. unfold Max in |- *. simpl in |- *. exact less_MAX_imp. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq