proposition: Lemma is_LimSup_seq_unique (u : nat -> R) (l : Rbar) : is_LimSup_seq u l -> LimSup_seq u = l.
proof: Proof. move => H. rewrite /LimSup_seq. case: ex_LimSup_seq => lu Hu /=. apply is_LimSup_infSup_seq in H. apply is_LimSup_infSup_seq in Hu. rewrite -(is_inf_seq_unique _ _ Hu). by apply is_inf_seq_unique. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy