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