proposition: Lemma qle_opp x y: x <=q y -> (BQopp y) <=q (BQopp x).
proof: Proof. move => [xq yq lexy]; split; try apply: QSo => //. move/BQ_P: xq => [_ nxz /BZps_sBZ dxz _]. move/BQ_P: yq => [_ nyz /BZps_sBZ dyz _]. rewrite /BQle_aux /BQopp; aw; rewrite - BZopp_prod_l // - BZopp_prod_r //. by apply: zle_opp; rewrite (BZprodC (Q y)) (BZprodC (P y)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)