proposition: Lemma derive_Rball_const : forall k c r x pr, derive_Rball c r (fun _ => k) pr x = 0.
proof: Proof. intros k c r x pr ; unfold derive_Rball ; destruct (in_Rball_dec c r x) as [x_in | x_nin] ; [apply derive_pt_Rball_const | reflexivity] ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics