proposition: Lemma BQ_of_pair_spos a b: inc a BZps -> inc b BZps -> inc (BQ_of_pair a b) BQps.
proof: Proof. move/BZps_iP => [ap an0] bzp; move:(BQ_of_pair_pos ap bzp) => h. by apply/BQps_iP; split => // /(BQ_of_pair_zero (BZp_sBZ ap) bzp). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)