proposition: Lemma rlt_opp x y: x <r y -> (BRopp y) <r (BRopp x).
proof: Proof. move => [pa pb]; split; first by apply:rle_opp. by move: pa => [xz yz _] pc; case: pb; apply:BRopp_inj. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)