proposition: Lemma derivable_pt_ext : forall x, derivable_pt f x -> derivable_pt g x.
proof: Proof. intros x [df Hdf] ; exists df ; apply derivable_pt_lim_ext ; trivial. Qed.
imports: Reals Rsequence_def Rpser_def Rpser_def_simpl Rpser_base_facts Rpser_sums Rpser_cv_facts Rinterval Ranalysis_def Rfunction_facts Tactics