proposition: Lemma Lim_seq_opp (u : nat -> R) : Lim_seq (fun n => - u n) = Rbar_opp (Lim_seq u).
proof: Proof. rewrite /Lim_seq. rewrite LimSup_seq_opp LimInf_seq_opp. case: (LimInf_seq u) => [li | | ] ; case: (LimSup_seq u) => [ls | | ] //= ; apply f_equal ; field. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy