proposition: Lemma derive_pt_f_eq_g f g x r (Hfg : forall y, r < y -> g y = f y) (rltx : r < x) (derivable_f : derivable_pt f x) : derive_pt f x (derivable_f) = derive_pt g x (derivable_f_eq_g Hfg rltx derivable_f).
proof: Proof. rewrite /derive_pt /derivable_f_eq_g. by destruct derivable_f. Qed.
imports: mathcomp(all_ssreflect) mathcomp(Rstruct) Reals Lra ssrR logb Reals_ext