proposition: Lemma BRopp_div_r x y: realp x -> realp y -> BRopp (x /r y) = x /r (BRopp y).
proof: Proof. move => xr yr; rewrite /BRdiv (BRinv_opp yr) BRopp_prod_r //; exact: RS_inv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)