proposition: Lemma max_one_ap_zero : forall x : IR, Max x [1] [#] [0].
proof: Proof. intros. apply ap_symmetric_unfolded. apply less_imp_ap. 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