proposition: Lemma pos_max_one : forall x : IR, [0] [<] Max x [1].
proof: Proof. intro. apply less_leEq_trans with OneR; [ apply pos_one | apply rht_leEq_Max ]. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq