proposition: Lemma Max_minus_eps_leEq : forall x y e, [0] [<] e -> {Max x y[-]e [<=] x} + {Max x y[-]e [<=] y}.
proof: Proof. intros. cut (Max x y[-]e [<] x or Max x y[-]e [<] y). intro H0; elim H0; intros; clear H0. left; apply less_leEq; assumption. right; apply less_leEq; assumption. apply less_Max_imp. apply shift_minus_less. apply shift_less_plus'. astepl ZeroR; assumption. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq