proposition: Lemma continuity_pt_locally_ext : forall f g a x, 0 < a -> (forall y, Rdist y x < a -> f y = g y) -> continuity_pt f x -> continuity_pt g x.
proof: Proof. intros f g a x a0 q cf eps ep. destruct (cf eps ep) as [a' [a'p Pa']]. exists (Rmin a a'); split. - unfold Rmin; destruct (Rle_dec a a'). + assumption. + assumption. - intros y cy; rewrite <- !q. + apply Pa'. split;[| apply Rlt_le_trans with (Rmin a a');[ | apply Rmin_r]];tauto. + rewrite Rdist_eq; assumption. + apply Rlt_le_trans with (Rmin a a');[ | apply Rmin_l]; tauto. Qed.
imports: Rbase Rfunctions Rlimit Rderiv