proposition: Lemma derivable_pt_lim_Rball_change : forall c r c' r' f x l, Rball c' r' x -> derivable_pt_lim_in (Rball c' r') f x l -> derivable_pt_lim_in (Rball c r) f x l.
proof: Proof. intros ; apply derivable_pt_lim_derivable_pt_lim_in ; eapply derivable_pt_lim_Rball_pt_lim ; eassumption. Qed.
imports: Reals Rpow_facts Rfunction_def Rinterval Rextensionality Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity Lra MyRIneq Rsequence_facts Rsequence_sums_facts RFsequence RFsequence_facts Rpser_def Rpser_base_facts Rpser_radius_facts Rpser_sums Rpser_sums_facts Tactics