proposition: Lemma derive_pt_ext (x : R) (prf : derivable_pt f x) (prg : derivable_pt g x) : derive_pt f x prf = derive_pt g x prg.
proof: Proof. apply pr_nu_var2 ; assumption. Qed.
imports: Reals Rsequence_def Rpser_def Rpser_def_simpl Rpser_base_facts Rpser_sums Rpser_cv_facts Rinterval Ranalysis_def Rfunction_facts Tactics