proposition: Lemma rle_oppP x y: realp x -> realp y -> ((BRopp y) <=r (BRopp x) <-> x <=r y).
proof: Proof. move => xr yr; split; last apply: rle_opp. by move => h;move:(rle_opp h); rewrite ! BRopp_K. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)