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