proposition: Lemma BQopp_negative1 x: inc x BQms -> inc (BQopp x) BQps.
proof: Proof. move => /Zo_P [xq xn]; apply/Zo_i; first by apply: QSo. by rewrite /BQopp; aw;apply/BZopp_negative1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)