proposition: Lemma ex_lim_seq_opp (u : nat -> R) : ex_lim_seq u <-> ex_lim_seq (fun n => -u n).
proof: Proof. split ; case => l Hl ; exists (Rbar_opp l). by apply -> is_lim_seq_opp. apply is_lim_seq_ext with (fun n => - - u n). move => n ; by apply Ropp_involutive. by apply -> is_lim_seq_opp. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy