proposition: Lemma BRdiv_square a b: realp a -> realp b -> BRsquare (a /r b) = (BRsquare a) /r (BRsquare b).
proof: Proof. move => ar br; rewrite /BRsquare /BRdiv. have ibr:= (RS_inv br). rewrite (BRprod_ACA ar ibr ar ibr). by rewrite (BRprod_inv br br). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)