proposition: Lemma continuity_pt_eq_compat : forall f g x, (exists alp, alp > 0 /\ forall y, R_dist x y < alp -> f y = g y) -> continuity_pt f x -> continuity_pt g x.
proof: Proof. intros f g x [alp1 [Halp1 H1]] H. intros eps Heps. destruct (H eps Heps) as [alp2 [Halp2 H2]]. exists (Rmin alp1 alp2); split. apply Rmin_pos_lt; assumption. intros u Hu. repeat rewrite <- H1. apply H2. split; intuition. unfold Rmin in * |- ; destruct Rle_dec; lra. rewrite R_dist_eq; assumption. apply Rlt_le_trans with (Rmin alp1 alp2). destruct Hu as [_ Hu]. rewrite R_dist_sym; apply Hu. apply Rmin_l. Qed.
imports: Reals MyReals Rsequence_def Rsequence_facts Rsequence_sums_facts Rseries_def Rpser_def Rpser_sums Rpser_sums_facts Rpser_derivative Rpser_radius_facts Rpser_taylor Lra Rintegral Rseries_facts Rseries_RiemannInt Rsequence_subsequence Rtactic