proposition: Lemma continuous_cos x : continuous cos x.
proof: Proof. apply continuity_pt_filterlim. by apply: continuity_cos => // . Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp