proposition: Lemma included_Rball_open_interval : forall c r, included (Rball c r) (open_interval (c - r) (c + r)).
proof: Proof. intros c r x H ; assert (H' := Rabs_def2 _ _ H) ; destruct H' ; split ; lra. Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics