proposition: Lemma BQ_of_pair_zero a b: intp a -> inc b BZps -> (BQ_of_pair a b) = \0q -> a = \0z.
proof: Proof. rewrite /BQ_of_pair -lock /BQ_of_pair_internal. move => az bzp /pr1_def h. by move: (proj1 (BZgcd_div az (BZps_sBZ bzp))); rewrite h BZprod_0r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)