proposition: Lemma RpSa x: realp x -> inc (BRabs x) BRp.
proof: Proof. case/BR_i0P => h; last by rewrite (BRabs_pos h). rewrite (BRabs_negs h); apply: (BRopp_negative2 (BRms_sBRm h)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)