proposition: Lemma single_limit : forall (f:R -> R) (D:R -> Prop) (l l' x0:R), adhDa D x0 -> limit1_in f D l x0 -> limit1_in f D l' x0 -> l = l'.
proof: Proof. unfold limit1_in; unfold limit_in; intros. simpl in *. cut (forall eps:R, eps > 0 -> dist R_met l l' < 2 * eps). - clear H0 H1; unfold dist in |- *; unfold R_met; unfold Rdist in |- *; unfold Rabs; case (Rcase_abs (l - l')) as [Hlt|Hge]; intros. + cut (forall eps:R, eps > 0 -> - (l - l') < eps). * intro; generalize (prop_eps (- (l - l')) H1); intro; generalize (Ropp_gt_lt_0_contravar (l - l') Hlt); intro; unfold Rgt in H3; generalize (Rgt_not_le (- (l - l')) 0 H3); intro; exfalso; auto. * intros; cut (eps * / 2 > 0). -- intro; generalize (H0 (eps * / 2) H2); rewrite (Rmult_comm eps (/ 2)); rewrite <- (Rmult_assoc 2 (/ 2) eps); rewrite (Rinv_r 2). ++ elim (Rmult_ne eps); intros a b; rewrite b; clear a b; trivial. ++ apply (Rlt_dichotomy_converse 2 0); right; generalize Rlt_0_1; intro; unfold Rgt; generalize (Rplus_lt_compat_l 1 0 1 H3); intro; elim (Rplus_ne 1); intros a b; rewrite a in H4; clear a b; apply (Rlt_trans 0 1 2 H3 H4). -- unfold Rgt; unfold Rgt in H1; rewrite (Rmult_comm eps (/ 2)); rewrite <- (Rmult_0_r (/ 2)); apply (Rmult_lt_compat_l (/ 2) 0 eps); auto. apply (Rinv_0_lt_compat 2); cut (1 < 2). ++ intro; apply (Rlt_trans 0 1 2 Rlt_0_1 H2). ++ generalize (Rplus_lt_compat_l 1 0 1 Rlt_0_1); elim (Rplus_ne 1); intros a b; rewrite a; clear a b; trivial. + cut (forall eps:R, eps > 0 -> l - l' < eps). * intro; generalize (prop_eps (l - l') H1); intro; elim (Rle_le_eq (l - l') 0); intros a b; clear b; apply (Rminus_diag_uniq l l'); apply a; split. -- assumption. -- apply (Rge_le (l - l') 0 Hge). * intros; cut (eps * / 2 > 0). -- intro; generalize (H0 (eps * / 2) H2); rewrite (Rmult_comm eps (/ 2)); rewrite <- (Rmult_assoc 2 (/ 2) eps); rewrite (Rinv_r 2). ++ elim (Rmult_ne eps); intros a b; rewrite b; clear a b; trivial. ++ apply (Rlt_dichotomy_converse 2 0); right; generalize Rlt_0_1; intro; unfold Rgt; generalize (Rplus_lt_compat_l 1 0 1 H3); intro; elim (Rplus_ne 1); intros a b; rewrite a in H4; clear a b; apply (Rlt_trans 0 1 2 H3 H4). -- unfold Rgt; unfold Rgt in H1; rewrite (Rmult_comm eps (/ 2)); rewrite <- (Rmult_0_r (/ 2)); apply (Rmult_lt_compat_l (/ 2) 0 eps); auto. apply (Rinv_0_lt_compat 2); cut (1 < 2). ++ intro; apply (Rlt_trans 0 1 2 Rlt_0_1 H2). ++ generalize (Rplus_lt_compat_l 1 0 1 Rlt_0_1); elim (Rplus_ne 1); intros a b; rewrite a; clear a b; trivial. - intros; unfold adhDa in H; elim (H0 eps H2); intros; elim (H1 eps H2); intros; clear H0 H1; elim H3; elim H4; clear H3 H4; intros; simpl; simpl in H1, H4; generalize (Rmin_Rgt x x1 0); intro; elim H5; intros; clear H5; elim (H (Rmin x x1) (H7 (conj H3 H0))); intros; elim H5; intros; clear H5 H H6 H7; generalize (Rmin_Rgt x x1 (Rdist x2 x0)); intro; elim H; intros; clear H H6; unfold Rgt in H5; elim (H5 H9); intros; clear H5 H9; generalize (H1 x2 (conj H8 H6)); generalize (H4 x2 (conj H8 H)); clear H8 H H6 H1 H4 H0 H3; intros; generalize (Rplus_lt_compat (Rdist (f x2) l) eps (Rdist (f x2) l') eps H H0); unfold Rdist; intros; rewrite (Rabs_minus_sym (f x2) l) in H1; rewrite (Rmult_comm 2 eps); replace (eps *2) with (eps + eps) by ring; generalize (Rdist_tri l l' (f x2)); unfold Rdist; intros; apply (Rle_lt_trans (Rabs (l - l')) (Rabs (l - f x2) + Rabs (f x2 - l')) (eps + eps) H3 H1). Qed.
imports: Rbase Rfunctions Lra