proposition: Lemma RmsS_inv x: inc x BRms -> inc (BRinv x) BRms.
proof: Proof. move => h;move:(BRms_sBR h) => h'. rewrite - (BRopp_K h') (BRinv_opp (RSo h')); apply:BRopp_positive1. exact:(RpsS_inv (BRopp_negative1 h)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)