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