proposition: Lemma LimSup_seq_opp (u : nat -> R) : LimSup_seq (fun n => - u n) = Rbar_opp (LimInf_seq u).
proof: Proof. rewrite LimSup_InfSup_seq LimInf_SupInf_seq. rewrite Inf_opp_sup ; apply f_equal, Sup_seq_ext => m. rewrite Inf_opp_sup ; by apply f_equal, Sup_seq_ext => n. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy