proposition: Lemma BQ_of_pair_sneg a b: inc a BZms -> inc b BZps -> inc (BQ_of_pair a b) BQms.
proof: Proof. move/BZms_iP => [ap an0] bzp; move:(BQ_of_pair_neg ap bzp) => h. by apply/BQms_iP; split => // /(BQ_of_pair_zero (BZm_sBZ ap) bzp). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)