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