proposition: Lemma BZdvd_exact b q: intp q -> intp b -> b <> \0z -> ((q *z b) %/z b = q /\ (q *z b) %%z b = \0z).
proof: Proof. move => qz bz bnz; move: (ZSp qz bz);set a := (q *z b) => az. have aux: (P a) %%c (P b) = \0c. move: (cdivides_pr1 (BZ_valN qz) (BZ_valN bz)) => [_ _]. by rewrite BZprod_val cprodC. split; last by rewrite (BZrem_div1 az bz bnz aux). move: (BZquo_div1 az bz bnz aux); rewrite {1} /a BZprodC => h. symmetry; exact (BZprod_eq2l qz (ZS_quo az bz) bz bnz h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)