proposition: Lemma derivable_pt_lim_ext : forall x l, derivable_pt_lim f x l -> derivable_pt_lim g x l.
proof: Proof. intros x l Hl eps eps_pos ; destruct (Hl _ eps_pos) as [delta Hdelta] ; exists delta ; intros ; do 2 rewrite <- fg_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