proposition: Lemma QmsS_inv x: inc x BQms -> inc (BQinv x) BQms.
proof: Proof. move => xqm; move: (BQms_sBQ xqm) => xq. move: (BQopp_negative1 xqm) => /QpsS_inv. have [ha hb]: pairp (BQinv x) /\ intp (P (BQinv x)). rewrite (BQinv_neg xqm); split; fprops; aw. by move /BQ_P: xq => [_ _ /BZps_sBZ /ZSo dz _]. rewrite (BQinv_opp xq) => /BQopp_positive1. by rewrite /BQopp pr1_pair pr2_pair BZopp_K // ha. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)