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