proposition: Lemma derivable_f_eq_g (f g : R -> R) x r : (forall y, r < y -> g y = f y) -> r < x -> derivable_pt f x -> derivable_pt g x.
proof: Proof. move=> Hfg rltx. case => l Hl. exists l => eps Heps ; move : Hl => /(_ eps Heps) ; case ; case => delt delt_pos Hdelt. have aux : 0 < Rmin (x - r) delt. apply Rmin_case => // ; apply (@ltR_add2r r); by rewrite add0R addRC subRKC. exists (mkposreal (Rmin (x - r) delt) aux) => /= h hnot0 Rlthdelta. rewrite Hfg ; last first. rewrite -ltR_subl_addr. apply (@ltR_add2r (- r)). rewrite -addRA addRCA -/(_ - _) subRR addR0 addRC. apply (@leR_ltR_trans (Rabs h)); first by rewrite -Rabs_Ropp; apply Rle_abs. apply (@ltR_leR_trans (Rmin (- r + x) delt)) => //. by rewrite addRC. exact/geR_minl. rewrite Hfg //. apply Hdelt => //=. apply (@ltR_leR_trans (Rmin (x - r) delt)) => // ; exact/geR_minr. Defined.
imports: mathcomp(all_ssreflect) mathcomp(Rstruct) Reals Lra ssrR logb Reals_ext