proposition: Lemma interval_dist_bound: forall lb ub x : R, interval lb ub x -> forall h : R, Rabs h <= interval_dist lb ub x -> interval lb ub (x + h).
proof: Proof. intros lb ub x x_in h [h_bd | heq]. apply open_interval_interval, open_interval_dist_bound ; assumption. unfold Rabs in heq ; destruct (Rcase_abs h). split ; rewrite (Ropp_eq_compat_l _ _ heq). transitivity (x + - (x - lb)) ; [right ; ring |] ; apply Rplus_le_compat_l, Ropp_le_contravar, Rmin_l. transitivity (ub + - (interval_dist lb ub x)). apply Rplus_le_compat_r, x_in. transitivity (ub + - 0) ; [| right ; ring]. apply Rplus_le_compat_l, Ropp_le_contravar, interval_dist_pos ; assumption. split ; subst. transitivity (x + 0) ; [ring_simplify ; apply x_in |]. apply Rplus_le_compat_l, interval_dist_pos ; assumption. transitivity (x + (ub - x)) ; [| right ; ring]. apply Rplus_le_compat_l, Rmin_r. Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics