proposition: Lemma BRinv_div x y: realp x -> realp y -> BRinv (x /r y) = y /r x.
proof: Proof. move => xr yr. by rewrite /BRdiv (BRprod_inv xr (RS_inv yr)) (BRinv_K yr) BRprodC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)