proposition: Lemma continuous_div f g x: realp x -> g x <> \0r -> continuous_at f x -> continuous_at g x -> continuous_at (fun z => f z /r g z) x.
proof: Proof. move => xr gnz pa pb. apply:(continuous_prod xr pa); apply: (continuous_comp pb). apply: (continuous_inv (continuous_real xr pb) gnz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)