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