proposition: Lemma is_lim_seq_unique (u : nat -> R) (l : Rbar) : is_lim_seq u l -> Lim_seq u = l.
proof: Proof. move => Hu. rewrite /Lim_seq. replace l with (Rbar_div_pos (Rbar_plus l l) {| pos := 2; cond_pos := Rlt_R0_R2 |}) by (case: (l) => [x | | ] //= ; apply f_equal ; field). apply (f_equal (fun x => Rbar_div_pos x _)). apply f_equal2. apply is_LimSup_seq_unique. by apply is_lim_LimSup_seq. apply is_LimInf_seq_unique. by apply is_lim_LimInf_seq. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy