proposition: Lemma included_Rball_open_interval2 : forall lb ub, included (Rball (middle lb ub) (interval_size lb ub)) (open_interval lb ub).
proof: Proof. intros lb ub x x_in ; destruct (Rabs_def2 _ _ x_in) as [x_lb x_ub] ; split. apply Rle_lt_trans with (middle lb ub - interval_size lb ub). right ; unfold middle, interval_size ; field. lra. apply Rlt_le_trans with (middle lb ub + interval_size lb ub). lra. right ; unfold middle, interval_size ; field. Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics