proposition: Lemma BQ_of_pair_pos a b: inc a BZp -> inc b BZps -> inc (BQ_of_pair a b) BQp.
proof: Proof. move => azp bzps; move: (BZp_sBZ azp) (BZps_sBZ bzps) => az bz. apply:Zo_i; first exact: BQ_of_pair_prop4. by rewrite /BQ_of_pair -lock /BQ_of_pair_internal pr1_pair; apply :BZ_positive_quo_gcd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)