proposition: Lemma is_lim_seq_opp (u : nat -> R) (l : Rbar) : is_lim_seq u l <-> is_lim_seq (fun n => -u n) (Rbar_opp l).
proof: Proof. split ; move => Hu. apply is_LimSup_LimInf_lim_seq. apply is_LimSup_opp_LimInf_seq. by apply is_lim_LimInf_seq. apply is_LimInf_opp_LimSup_seq. by apply is_lim_LimSup_seq. apply is_LimSup_LimInf_lim_seq. apply is_LimInf_opp_LimSup_seq. by apply is_lim_LimInf_seq. apply is_LimSup_opp_LimInf_seq. by apply is_lim_LimSup_seq. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy