proposition: Lemma BZdvd_and_diff 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 => h1 h2; rewrite /BZdiff. move:(h2) => [a'z _ _ ]. rewrite - (BZquo_opp2 h2). move /(BZdvds_opp2 _ a'z): h2 => h3. exact (BZdvd_and_sum h1 h3). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)