proposition: Lemma derive_pt_in_ext_strong: forall (D : R -> Prop) f g x (prf: derivable_pt_in D f x) (prg: derivable_pt_in D g x), dense D x -> D x -> (forall x, D x -> f x = g x) -> derive_pt_in D f x prf = derive_pt_in D g x prg.
proof: Proof. intros D f g x [l1 Hl1] [l2 Hl2] dD x_in Heq ; simpl ; eapply derivable_pt_lim_in_uniqueness ; [eassumption | | eassumption]. 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