proposition: Lemma Lim_opp (f : R -> R) (x : Rbar) : Lim (fun y => - f y) x = Rbar_opp (Lim f x).
proof: Proof. rewrite -Lim_seq_opp. by apply Lim_seq_ext. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq