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