proposition: Lemma derive_pt_Rball_const : forall k c r x pr, Rball c r x -> derive_pt_in (Rball c r) (fun _ => k) x pr = 0.
proof: Proof. intros k c r x pr x_in ; eapply derivable_pt_lim_in_derive_pt_Rball ; [eexact x_in | eapply derivable_pt_lim_in_const]. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics