proposition: Lemma is_LimInf_supInf_seq (u : nat -> R) (l : Rbar) : is_LimInf_seq u l <-> is_sup_seq (fun m => Inf_seq (fun n => u (n + m)%nat)) l.
proof: Proof. rewrite -is_LimSup_opp_LimInf_seq. rewrite is_LimSup_infSup_seq. rewrite -is_sup_opp_inf_seq. rewrite Rbar_opp_involutive. split ; apply is_sup_seq_ext => n ; by rewrite Inf_opp_sup. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy