proposition: Lemma is_lim_plus' (f g : R -> R) (x : Rbar) (lf lg : R) : is_lim f x lf -> is_lim g x lg -> is_lim (fun y => f y + g y) x (lf + lg).
proof: Proof. intros Hf Hg. eapply is_lim_plus. by apply Hf. by apply Hg. by []. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq