proposition: Lemma RS_inv x: realp x -> realp (BRinv x).
proof: Proof. case /BR_i1P => xs. + rewrite xs BRinv_0; apply:RS0. + exact: (BRps_sBR (RpsS_inv xs)). + exact: (BRms_sBR(RmsS_inv xs)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)