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