proposition: Lemma is_lim_opp (f : R -> R) (x l : Rbar) : is_lim f x l -> is_lim (fun y => - f y) x (Rbar_opp l).
proof: Proof. intros Cf. eapply filterlim_comp. apply Cf. apply filterlim_Rbar_opp. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq