proposition: Lemma continuous2_div x y: realp x -> realp y -> (continuous_at (BRdiv ^~y) x) /\(y <> \0r -> continuous_at (BRdiv x) y).
proof: Proof. move => xr yr; rewrite /BRdiv. move:(continuous2_prod xr (RS_inv yr)) => [sa sb]. split => // ynz; exact:(continuous_comp (continuous_inv yr ynz) sa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)