proposition: Lemma BR_self_inv x: realp x -> (x = BRinv x <-> [\/ x= \0r, x = \1r | x = \1mr]).
proof: Proof. move => xr; split. move => h; case: (equal_or_not x \0r) => e0; first by constructor 1. move: (f_equal (fun z => x *r z) h). rewrite (BRprod_inv1 xr e0) => /(BR_square_1 xr). by case => hh;[constructor 2 | constructor 3]. by case => ->; [rewrite BRinv_0 | rewrite BRinv_1 | rewrite BRinv_m1 ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)