proposition: Lemma BRdiv_opp_opp x y: realp x -> realp y -> (BRopp x) /r (BRopp y) = x /r y.
proof: Proof. move => xr yr. by rewrite -(BRopp_div_l xr (RSo yr)) - BRopp_div_r // BRopp_K //; apply:RS_div. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)