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