proposition: Lemma BR_inv_prop a b: realp a -> realp b -> a *r b = \1r -> b = BRinv a.
proof: Proof. move => ar br h. have ha:= RS_inv ar. case: (equal_or_not a \0r) => aq. by move: h; rewrite aq BRprod_0l // => hh; case:BR_one_nz. move: (f_equal (fun z => (BRinv a) *r z) h). rewrite BRprodA // BRprod_1r // (BRprodC _ a) (BRprod_inv1) // BRprod_1l //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)