proposition: Lemma BZdvds_pr a b: b %|z a -> a = b *z (a %/z b).
proof: Proof. move => [pa pb pd]. move: pd; rewrite /BZrem => h. exact (BZdiff_diag_rw pa (ZSp pb (ZS_quo pa pb)) h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)