proposition: Lemma limit1_in_ext: forall (D : R -> Prop) f g x l, (forall x, D x -> f x = g x) -> limit1_in f D l x -> limit1_in g D l x.
proof: Proof. intros D f g x l Heq Hf eps eps_pos ; destruct (Hf _ eps_pos) as [alp [alp_pos Halp]] ; exists alp ; split ; [assumption |]. intros y Hy ; rewrite <- Heq ; [apply Halp |] ; apply Hy. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Ranalysis_def Rfunction_facts MyRIneq MyR_dist Lra