proposition: Lemma continuous_Rabs_comp f (x : R) : continuous f x -> continuous (fun x0 => Rabs (f x0)) x.
proof: Proof. move => Hcontfx. apply: continuous_comp => // . apply: continuous_Rabs. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp