proposition: Lemma BRdiv_prod x y:realp x -> realp y -> x <> \0r -> (x *r y) /r x = y.
proof: Proof. move => xr yr h. rewrite /BRdiv BRprodC (BRprodA (RS_inv xr) xr yr). by rewrite (BRprodC _ x) BRprod_inv1 // BRprod_1l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)