proposition: Lemma open_interval_dist_bound: forall lb ub x, interval lb ub x -> forall h, Rabs h < interval_dist lb ub x -> open_interval lb ub (x + h).
proof: Proof. intros lb ub x x_in h h_bd ; assert (H := Rabs_def2 _ _ h_bd) ; destruct H as [x_lb x_ub]. assert (H1: - (x - lb) < h). apply Rle_lt_trans with (- Rmin (x - lb) (ub - x)). apply Ropp_le_contravar, Rmin_l. assumption. assert (H2: h < ub - x). apply Rlt_le_trans with (Rmin (x - lb) (ub - x)). assumption. apply Rmin_r. split ; clear -H1 H2 ; lra. Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics