proposition: Lemma BQnum0_P1 x: inc x BZps -> (BQ_of_pair \0z x) = \0q.
proof: Proof. move => xp; move:(BZps_sBZ xp) => xz. move/BZps_iP: xp => [xp xnz]. rewrite /BQ_of_pair -lock /BQ_of_pair_internal /BQ_zero BZgcd_C BZgcd_zero //. rewrite (BZabs_pos xp) (proj2 (BZ_quorem00 xz)). by rewrite/ BQ_of_Z (proj2 (BZdvd_itself xz xnz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)