proposition: Lemma BRdiv_prod_simpl_r x y z: realp x -> realp y -> realp z -> z <> \0r -> (x *r z) /r (y *r z) = x /r y.
proof: Proof. move => xr yr rz h; rewrite (BRprodC x z) (BRprodC y z). by apply: BRdiv_prod_simpl_l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)