proposition: Lemma Rfun_continuity_pt_eq_compat : forall x, continuity_pt f x -> continuity_pt g x.
proof: Proof. intros x Hct eps H. specialize (Hct eps H). destruct Hct as (alp & pos & HH). exists alp. split; auto. intros x0 H0. specialize (HH x0 H0). eauto. repeat rewrite <-Heq. auto. Qed.
imports: Reals Rfunction_def