proposition: Lemma continuous_cos_comp (f : R -> R) x: continuous f x -> continuous (fun x => cos (f x)) x.
proof: Proof. move => Hcont. apply: continuous_comp => //. by apply: continuous_cos. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp