proposition: Lemma continuous_Rdiv_1_x x (H : x <> 0) : continuous (Rdiv 1) x.
proof: Proof. apply: (continuous_ext (fun (x : R) => (/ x))). by move => x0; rewrite /Rdiv Rmult_1_l. exact: continuous_Rinv. Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval