proposition: Lemma continuous_plus (f g : U -> V) (x : U) : continuous f x -> continuous g x -> continuous (fun x : U => plus (f x) (g x)) x.
proof: Proof. intros. eapply filterlim_comp_2. by apply H. by apply H0. apply (filterlim_plus (f x) (g x)). Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq