proposition: Lemma is_LimInf_seq_unique (u : nat -> R) (l : Rbar) : is_LimInf_seq u l -> LimInf_seq u = l.
proof: Proof. move => H. rewrite /LimInf_seq. case: ex_LimInf_seq => lu Hu /=. apply is_LimInf_supInf_seq in H. apply is_LimInf_supInf_seq in Hu. rewrite -(is_sup_seq_unique _ _ Hu). by apply is_sup_seq_unique. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy