proposition: Lemma BRdiv_prod_simpl_l x y z: realp x -> realp y -> realp z -> x <> \0r -> (x *r y) /r (x *r z) = y /r z.
proof: Proof. move => xr yr zr xnz. rewrite /BRdiv (BRprod_inv xr zr) (BRprodC x y). rewrite (BRprodA (RSp yr xr) (RS_inv xr) (RS_inv zr)). by rewrite -(BRprodA yr xr (RS_inv xr)) BRprod_inv1 // BRprod_1r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)