proposition: Lemma included_open_interval_Rball : forall lb ub, included (open_interval lb ub) (Rball (middle lb ub) (interval_size lb ub)).
proof: Proof. intros lb ub x x_in ; apply Rabs_def1. apply Rlt_minus_sort, Rlt_le_trans with ub. apply x_in. unfold middle, interval_size ; right ; field. apply Rlt_minus_sort2, Rle_lt_trans with lb. unfold middle, interval_size ; right ; field. apply x_in. Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics