proposition: Lemma BRdiv_prod_comm x y z: realp x -> realp y -> realp z -> (x *r y) /r z = (x /r z) *r y.
proof: Proof. move => xr yr zr. rewrite /BRdiv (BRprodC x y) (BRprodC _ y) - (BRprodA yr xr) //; exact:RS_inv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)