proposition: Lemma BZdvds_prod a b c: intp a -> intp b -> intp c -> c <> \0z -> ( a %|z b <-> (a *z c) %|z (b *z c)).
proof: Proof. move => az bz cz cnz. move: (ZS_quo bz az) => baz. split => h. rewrite (BZdvds_pr h) (BZprodC a (b %/z a)) -(BZprodA baz az cz). apply:(BZdvds_pr1 baz (ZSp az cz)); apply: BZprod_nz => //. move: (BZdvds_pr h). move: (ZS_quo (ZSp bz cz)(ZSp az cz)). set t := (b *z c) %/z (a *z c) => tz. rewrite (BZprodC a) (BZprodC _ c) - (BZprodA cz az tz) => h1. rewrite (BZprod_eq2l bz (ZSp az tz) cz cnz h1) BZprodC. apply:(BZdvds_pr1 tz az). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)