proposition: Lemma BZquo_simplify a b c: intp a -> intp b -> inc c BZps -> ( (a *z c) %/z(b *z c) = a %/z b /\ (a *z c) %%z (b *z c) = (a %%z b) *z c).
proof: Proof. move => az bz czp. case (equal_or_not b \0z) => bnz. rewrite bnz BZprod_0l //. move: (BZ_quorem0 az) => [-> ->]. by move: (BZ_quorem0 (ZSp az (BZps_sBZ czp))) => [-> ->]. move:(BZdvd_correct az bz bnz); set q := a %/z b; set r := (a %%z b). move => [qz rzp [qr r0 r1]]. move: (BZps_sBZ czp)(BZp_sBZ rzp) => cz rz. move /BZps_iP: (czp) => [pa pb]. move: (ZpS_prod rzp pa) => pc. have pd: a *z c = (b *z c) *z q +z r *z c. rewrite qr (BZprodDl cz (ZSp bz qz) rz). by rewrite BZprodC (BZprodA cz bz qz) (BZprodC c). have pe: r *z c <z BZabs (b *z c). rewrite (BZprod_abs bz cz) (BZabs_pos pa). by apply /(BZprod_plt2r rz (ZSa bz) czp). have bcnz: (b *z c) <> \0z. by apply: BZprod_nz => //;move /BZps_iP: czp => [_]. have h: (BZdivision_prop (a *z c) (b *z c) q (r *z c)) by split => //. move: (BZdvd_unique1 (ZSp az cz) (ZSp bz cz) qz (ZSp rz cz) bcnz h). by move => [-> ->]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)