proposition: Lemma derivable_ext : derivable f -> derivable g.
proof: Proof. intros f_deriv x ; apply derivable_pt_ext ; auto. Qed.
imports: Reals Rsequence_def Rpser_def Rpser_def_simpl Rpser_base_facts Rpser_sums Rpser_cv_facts Rinterval Ranalysis_def Rfunction_facts Tactics