proposition: Lemma BZdvds_pr1 a b: intp a -> intp b -> b %|z (a *z b).
proof: Proof. move => pa pb; case: (equal_or_not b \0z) => H. rewrite H BZprod_0r; apply:BZdvds_trivial. by move:(BZdvd_exact pa pb H) => [_ dd]; split => //;apply: ZSp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)