proposition: Theorem derivable_pt_lim_eq_locally : forall f g x l, locally_true x (fun v => f v = g v) -> derivable_pt_lim f x l -> derivable_pt_lim g x l.
proof: Proof. intros f g x l (delta1, (Hd, Heq)) Hf eps Heps. destruct (Hf eps Heps) as (delta2, H0). clear Hf. assert (0 < Rmin delta1 delta2)%R. apply Rmin_pos. exact Hd. exact (cond_pos delta2). exists (mkposreal (Rmin delta1 delta2) H). intros. rewrite <- Heq. pattern x at 2 ; rewrite <- Rplus_0_r. rewrite <- Heq. rewrite Rplus_0_r. apply H0. exact H1. apply Rlt_le_trans with (1 := H2). simpl. apply Rmin_r. rewrite Rabs_R0. exact Hd. apply Rlt_le_trans with (1 := H2). simpl. apply Rmin_l. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux)