proposition: Lemma derivable_pt_in_ext_strong : forall f g (D : R -> Prop) x, D x -> (forall x, D x -> f x = g x) -> derivable_pt_in D f x -> derivable_pt_in D g x.
proof: Proof. intros f g D x Dx Heq [l Hl] ; exists l ; eapply derivable_pt_lim_in_ext_strong ; eassumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics