proposition: Lemma derive_Rball_derive : forall f c r x pr pr', Rball c r x -> derive_Rball c r f pr x = derive f pr' x.
proof: Proof. intros f c r x pr pr' x_in ; unfold derive_Rball, derive. destruct (in_Rball_dec c r x). apply derive_Rball_pt ; assumption. contradiction. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics