proposition: Lemma BZdvds_trans1 a b a': a %|z a'-> b %|z a -> a' %/z b = (a' %/z a) *z (a %/z b).
proof: Proof. move => pa pb. rewrite {1} (BZdvds_pr pa) {1} (BZdvds_pr pb). move: pa pb => [a'z az _ ] [_ bz _]. case: (equal_or_not b \0z) => bnz; first by rewrite bnz !BZ_quo0 BZprod_0r. move: (ZS_quo az bz)(ZS_quo a'z az) => qa qb. by rewrite - (BZprodA bz qa qb) (BZdvds_pr5 bz (ZSp qa qb) bnz) BZprodC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)