proposition: Lemma LimInf_SupInf_seq (u : nat -> R) : LimInf_seq u = Sup_seq (fun m => Inf_seq (fun n => u (n + m)%nat)).
proof: Proof. apply is_LimInf_seq_unique. apply is_LimInf_supInf_seq. rewrite /Sup_seq. by case: ex_sup_seq. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy