proposition: Lemma derivable_pt_lim_locally_ext : forall f g x a b l, a < x < b -> (forall z, a < z < b -> f z = g z) -> derivable_pt_lim f x l -> derivable_pt_lim g x l.
proof: Proof. intros f g x a b l axb fg df e ep. destruct (df e ep) as [d pd]. assert (d'h : 0 < Rmin d (Rmin (b - x) (x - a))). - apply Rmin_pos;[apply cond_pos | apply Rmin_pos; apply Rlt_0_minus; tauto]. - exists (mkposreal _ d'h); simpl; intros h hn0 cmp. rewrite <- !fg;[ |assumption | ]. + apply pd;[assumption |]. apply Rlt_le_trans with (1 := cmp), Rmin_l. + assert (-h < x - a). * apply Rle_lt_trans with (1 := Rle_abs _). rewrite Rabs_Ropp; apply Rlt_le_trans with (1 := cmp). rewrite Rmin_assoc; apply Rmin_r. * assert (h < b - x). -- apply Rle_lt_trans with (1 := Rle_abs _). apply Rlt_le_trans with (1 := cmp). rewrite Rmin_comm, <- Rmin_assoc; apply Rmin_l. -- split. ++ apply (Rplus_lt_reg_l (- h)). replace ((-h) + (x + h)) with x by ring. apply (Rplus_lt_reg_r (- a)). replace (((-h) + a) + - a) with (-h) by ring. assumption. ++ apply (Rplus_lt_reg_r (- x)). replace (x + h + - x) with h by ring. assumption. Qed.
imports: Rbase Rfunctions Rlimit Rderiv