proposition: Lemma limit1_in_ext_strong: forall (D : R -> Prop) r f g x l, 0 < r -> (forall y, Rball x r y -> D y -> f y = g y) -> limit1_in f D l x -> limit1_in g D l x.
proof: Proof. intros D alp f g x l alp_pos Heq Hf eps eps_pos ; destruct (Hf _ eps_pos) as [bet [bet_pos Hbet]] ; exists (Rmin alp bet) ; split. apply Rmin_pos_lt ; assumption. intros y [Dy y_bd] ; rewrite <- Heq. apply Hbet ; split ; [assumption | apply Rlt_le_trans with (Rmin alp bet) ; [assumption | apply Rmin_r]]. apply Rlt_le_trans with (Rmin alp bet) ; [apply y_bd | apply Rmin_l]. assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Ranalysis_def Rfunction_facts MyRIneq MyR_dist Lra