proposition: Lemma BRprod_inv x y:realp x -> realp y -> BRinv (x *r y) = BRinv x *r BRinv y.
proof: Proof. move => xr yr. have pc :=RS_inv xr. have pd :=RS_inv yr. case: (equal_or_not x \0r) => xz. by rewrite xz BRinv_0 BRprod_0l BRinv_0 BRprod_0l. case: (equal_or_not y \0r) => yz. by rewrite yz BRinv_0 BRprod_0r BRinv_0 BRprod_0r. symmetry; apply:BR_inv_prop; try apply:RSp => //. rewrite BRprod_ACA // !BRprod_inv1 // BRprod_1l //; apply: RS1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)