proposition: Lemma continuity_ext : continuity f -> continuity g.
proof: Proof. intros f_cont x eps eps_pos. destruct (f_cont x _ eps_pos) as [delta [delta_pos Hdelta]]. exists delta ; split ; [assumption |]. 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