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