proposition: Lemma BZdvd_and_sum a a' b: b %|z a -> b %|z a' -> ( b %|z (a +z a') /\ (a +z a') %/z b = (a %/z b) +z (a' %/z b)).
proof: Proof. move => pa pb; move: (BZdvds_pr pa) (BZdvds_pr pb). set q1 := a %/z b; set q2:= a' %/z b => e1 e2. move: pa pb => [az bz _] [a'z _ _]. move: (ZS_quo az bz)(ZS_quo a'z bz) => q1z q2z. have -> : a +z a' = b *z (q1 +z q2). by rewrite e1 e2 (BZprodDr bz q1z q2z). case: (equal_or_not b \0z) => bnz. rewrite /q1 /q2 bnz !BZ_quo0 (BZsum_0r ZS0) BZprod_0r. split => //; apply: BZdvds_trivial. rewrite (BZdvds_pr5 bz (ZSs q1z q2z) bnz);split => //. rewrite BZprodC;apply: (BZdvds_pr1 (ZSs q1z q2z) bz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)