proposition: Lemma BRprod_eq2r x y z: realp x -> realp y -> realp z -> z <> \0r -> x *r z = y *r z -> x = y.
proof: Proof. move => xr yr zr zp h. by rewrite - (BRdiv_prod zr xr zp) - (BRdiv_prod zr yr zp) BRprodC h BRprodC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)