proposition: Lemma qle_oppP x y: ratp x -> ratp y -> ((BQopp y) <=q (BQopp x) <-> x <=q y).
proof: Proof. move => xq yq; split; last apply: qle_opp. by move => h;move:(qle_opp h); rewrite ! BQopp_K. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)