proposition: Lemma derive_Rball_ext_strong: forall c r f g (prf: derivable_Rball c r f) (prg: derivable_Rball c r g), Rball_eq c r f g -> derive_Rball c r f prf == derive_Rball c r g prg.
proof: Proof. intros c r f g prf prg Heq x ; unfold derive_Rball ; destruct (in_Rball_dec c r x) as [HT1 | HF1]. eapply derive_pt_in_ext_strong ; [apply dense_Rball | |] ; assumption. reflexivity. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics