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