proposition: Lemma BRprodBl x y z: realp x -> realp y -> realp z -> (y -r z) *r x = (y *r x) -r (z *r x).
proof: Proof. by move => xz yz zr; rewrite BRprodC (BRprodC y) (BRprodC z) BRprodBr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)