proposition: Lemma is_C_lim_unique (f : C -> C) (z l : C) : filterlim f (locally' z) (locally l) -> C_lim f z = l.
proof: Proof. case: l => lx ly H. apply injective_projections ; simpl. apply (f_equal real (y := Finite lx)). apply is_lim_unique => /= P [eps Hp]. destruct (H (fun z => P (fst z))) as [delta Hd] ; clear H. exists eps => y Hy. apply Hp, Hy. exists delta. intros y By Hy. apply Hd. split ; simpl. apply By. apply ball_center. contradict Hy. clear -Hy. destruct z as [z1 z2]. now injection Hy. apply (f_equal real (y := Finite ly)). apply is_lim_unique => /= P [eps Hp]. destruct (H (fun z => P (snd z))) as [delta Hd] ; clear H. exists eps => y Hy. apply Hp. apply Hy. exists delta. intros y By Hy. apply Hd. split ; simpl. apply By. apply ball_center. contradict Hy. clear -Hy. destruct z as [z1 z2]. now injection Hy. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy