proposition: Lemma BRprod_AC 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. by rewrite - (BRprodA xr yr zr) - (BRprodA xr zr yr) (BRprodC y). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)