proposition: Lemma BRinv_abs x: realp x -> BRabs (BRinv x) = BRinv (BRabs x).
proof: Proof. move => xr. case/BR_i1P: (xr) => h. + by rewrite h BRabs_0 BRinv_0 BRabs_0. + by rewrite (BRabs_pos (BRps_sBRp(RpsS_inv h))) (BRabs_pos (BRps_sBRp h)). + by rewrite (BRabs_negs (RmsS_inv h)) (BRabs_negs h) (BRinv_opp xr). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)