proposition: Lemma continuity_pt_in_ext : forall D (f g : R -> R) x, (f == g)%F -> continuity_pt_in D f x -> continuity_pt_in D g x.
proof: Proof. intros D f g x Heq Hf Dx ; eapply limit1_in_ext. intros ; apply Heq. rewrite <- (Heq x) ; apply Hf ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Ranalysis_def Ranalysis_def_simpl Rfunction_facts MyRIneq MyR_dist Lra Tactics