proposition: Lemma Rball_dist_bound: forall c r x, Rball c r x -> forall h, Rabs h < Rball_dist c r x -> Rball c r (x + h).
proof: Proof. intros ; apply included_open_interval_Rball2, open_interval_dist_bound. eapply open_interval_interval, included_Rball_open_interval ; eassumption. assumption. Qed.
imports: Rbase Rfunctions Rfunction_def Rtopology Lra MyRIneq MyNeq PSeries_reg Tactics