proposition: Lemma BRabs_prop1 x y: realp x -> realp y -> (BRabs x <=r y <-> (BRopp y <=r x /\ x <=r y)).
proof: Proof. move => xr yr. case /BR_i0P: (xr) => xp. rewrite (BRabs_negs xp); move: (rle_oppP (RSo xr) yr);rewrite (BRopp_K xr). move => h. apply:(iff_trans (iff_sym h)); split; last by move => []. move => h1; split => //. move:(BRms_sBRm xp) => xp'. move:(rle_par3 (BRopp_negative2 xp') xp') => h2. move/h: h1 => h3; BRo_tac. rewrite (BRabs_pos xp); split; last by move => []. move => lxy; split => //; rewrite - (BRopp_K xr); apply: rle_opp. have h: BRopp x <=r x by apply:(rle_par3 xp (BRopp_positive2 xp)). BRo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)