proposition: Lemma derive_derive_Rball: forall c r f pr pr', Rball_eq c r (derive f pr) (derive_Rball c r f pr').
proof: Proof. intros c r f pr pr' x x_in ; unfold derive_Rball ; destruct (in_Rball_dec c r x) as [HT | HF]. destruct (pr' x HT) as [l Hl] ; simpl ; unfold derive ; rewrite derive_pt_eq ; eapply derivable_pt_lim_Rball_pt_lim ; eassumption. destruct (HF x_in). Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics