proposition: Lemma included_open_interval_Rball2 : forall c r, included (open_interval (c - r) (c + r)) (Rball c r).
proof: Proof. intros c r x [x_lb x_ub] ; apply Rabs_def1 ; lra. Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics