proposition: Lemma BRinv_diff x y: realp x -> realp y ->x <> \0r -> y <> \0r -> (BRinv x -r BRinv y) = (y -r x) /r (x *r y).
proof: Proof. move => xr yr xnz ynz. move:(RS_inv xr)(RS_inv yr) (RSp xr yr) (RS_diff yr xr) => ixr iyr xyr dr. move:(BRprod_nz xr yr xnz ynz) => xynz. apply:(BRprod_eq2r (RS_diff ixr iyr) (RS_div dr xyr) xyr xynz). rewrite (BRprod_div1 xyr dr xynz) (BRprodBl xyr ixr iyr). rewrite BRprodC -/(_ /r _) (BRdiv_prod xr yr xnz). by rewrite BRprodC -/(_ /r _)(BRprodC x y) (BRdiv_prod yr xr ynz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)