proposition: Lemma continuous_Rinv x : x <> 0 -> continuous (fun x => / x) x.
proof: Proof. move => Hxneq0. apply continuity_pt_filterlim. apply: continuity_pt_inv => // . apply continuity_pt_filterlim. apply: continuous_id. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp