proposition: Lemma BZdvd_pr2 a b q: inc q BZ -> intp b -> b <> \0z -> a = b *z q -> q = a %/z b.
proof: Proof. move => qz bz bnz pd. move: (ZSp bz qz); rewrite - pd => az. have hh: (BZdivision_prop a b q \0z). red; rewrite - pd (BZsum_0r az);split => //; last by apply: ZpS0. split; last by move => abz; case: bnz;apply: (BZabs_0p bz). apply /zle0xP; exact (BZabs_iN bz). exact (proj1 (BZdvd_unique1 az bz qz ZS0 bnz hh)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)