proposition: Lemma is_lim_unique (f : R -> R) (x l : Rbar) : is_lim f x l -> Lim f x = l.
proof: Proof. intros. unfold Lim. rewrite (is_lim_seq_unique _ l) //. apply (is_lim_comp_seq f _ x l H). exists 1%nat => n Hn. case: x {H} => [x | | ] //=. apply Rbar_finite_neq, Rgt_not_eq, Rminus_lt_0. ring_simplify. by apply RinvN_pos. by apply is_lim_seq_Rbar_loc_seq. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq