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