proposition: Lemma continuity_in_ext_strong : forall (D : R -> Prop) f g, (forall x, D x -> f x = g x)%F -> continuity_in D f -> continuity_in D g.
proof: Proof. intros D f g Heq Hf x ; eapply continuity_pt_in_ext_strong, Hf ; eassumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Ranalysis_def Ranalysis_def_simpl Rfunction_facts MyRIneq MyR_dist Lra Tactics