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