proposition: Lemma tech_limit : forall (f:R -> R) (D:R -> Prop) (l x0:R), D x0 -> limit1_in f D l x0 -> l = f x0.
proof: Proof. intros f D l x0 H H0. case (Rabs_pos (f x0 - l)); intros H1. - absurd ((@dist R_met) (f x0) l < (@dist R_met) (f x0) l). + apply Rlt_irrefl. + case (H0 ((@dist R_met) (f x0) l)); auto. intros alpha1 [H2 H3]; apply H3; auto; split; auto. case (dist_refl R_met x0 x0); intros Hr1 Hr2; rewrite Hr2; auto. - case (dist_refl R_met (f x0) l); intros Hr1 Hr2; symmetry; auto. Qed.
imports: Rbase Rfunctions Lra