proposition: Lemma qlt_opp x y: x <q y -> (BQopp y) <q (BQopp x).
proof: Proof. move => [lxy nxy]; split; first by apply:qle_opp. by move: lxy => [xq yq _] no; case: nxy; apply:BQopp_inj. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)