proposition: Lemma BQinv_neg x: inc x BQms -> BQinv x = J (BZopp (Qden x)) (BZopp (Qnum x)).
proof: Proof. move/Zo_P => [xQ /BZms_iP [px py]]. rewrite /BQinv;Ytac0; Ytac h => //; case: (BZ_di_pos_neg h px). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)