proposition: Lemma BQms_iP x: inc x BQms <-> inc x BQm /\ x <> \0q.
proof: Proof. split; first by move => h; split; [ apply:BQms_sBQm| apply: BQms_nz]. move => [ /Zo_P [xq nxn] xnz ]; apply: Zo_i => //. by apply/BZms_iP; split => //; move/(BQnum0_P xq). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)