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