proposition: Lemma derive_ext (prf : derivable f) (prg : derivable g) : derive f prf == derive g prg.
proof: Proof. intro x ; unfold derive ; apply derive_pt_ext. Qed.
imports: Reals Rsequence_def Rpser_def Rpser_def_simpl Rpser_base_facts Rpser_sums Rpser_cv_facts Rinterval Ranalysis_def Rfunction_facts Tactics