proposition: Lemma single_limit : forall f D l l' x, adhDa D x -> limit1_in f D l x -> limit1_in f D l' x -> l = l'.
proof: Proof. unfold limit1_in, limit_in ; intros f D l l' x HD Hl Hl' ; cut (forall eps:R, eps > 0 -> dist C_met l l' < eps). simpl ; unfold C_dist ; intro Hforall. apply Cseq_cv_unique with (fun _ => l). apply Cseq_cst_cv. intros eps eps_pos ; exists 0%nat ; intros n n_lb ; apply Hforall ; assumption. intros eps eps_pos ; assert (eps_2_pos : eps / 2 > 0) by lra ; destruct (Hl (eps / 2)%R eps_2_pos) as (alpha1, [alpha1_pos Halpha1]) ; destruct (Hl' (eps / 2)%R eps_2_pos) as (alpha2, [alpha2_pos Halpha2]) ; assert (alpha'_pos : Rmin alpha1 alpha2 > 0) by (apply Rmin_pos ; assumption) ; destruct (HD (Rmin alpha1 alpha2)%R alpha'_pos) as (x', [Dx' Hx']) ; clear Hl Hl' HD. apply Rle_lt_trans with (Cnorm (l - (f x')) + Cnorm (f x' - l'))%R. simpl ; unfold C_dist. replace (Cnorm (l - l')) with (Cnorm ((l - f x') + (f x' - l'))) by (apply Cnorm_eq_compat ; field) ; apply Cnorm_triang. apply Rlt_le_trans with (eps / 2 + eps / 2)%R ; [| right ; field] ; apply Rlt_trans with (Cnorm (l - f x') + eps / 2)%R. apply Rplus_lt_compat_l ; simpl in Halpha2 ; apply Halpha2 ; split ; [| apply Rlt_le_trans with (Rmin alpha1 alpha2) ; [| apply Rmin_r]] ; assumption. apply Rplus_lt_compat_r ; simpl in Halpha1 ; rewrite Cnorm_minus_sym ; apply Halpha1 ; split ; [| apply Rlt_le_trans with (Rmin alpha1 alpha2) ; [| apply Rmin_l]] ; assumption. Qed.
imports: Rlimit Cbase Ctacfield Cnorm Cprop_base Rsequence_def Csequence Csequence_facts Cfunctions