proposition: Lemma ex_lim_plus (f g : R -> R) (x : Rbar) : ex_lim f x -> ex_lim g x -> ex_Rbar_plus (Lim f x) (Lim g x) -> ex_lim (fun y => f y + g y) x.
proof: Proof. move => /Lim_correct Hf /Lim_correct Hg Hl. exists (Rbar_plus (Lim f x) (Lim g x)). eapply is_lim_plus ; try eassumption. by apply Rbar_plus_correct. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq