proposition: Lemma rle_abs x: realp x -> x <=r (BRabs x).
proof: Proof. move => xr;case /BR_i0P: (xr) => xp. move: (RpSa xr) => / rle0xP pa; move / rgt0xP: xp => [pb _]; BRo_tac. by rewrite (BRabs_pos xp); apply:rleR. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)