proposition: Lemma BZ_quorem0 a: intp a -> (a %%z \0z = a /\ a %/z \0z = \0z).
proof: Proof. move => pa; move:(BZ_quo0 a) => pb. by split => //; rewrite /BZrem pb /BZdiff BZprod_0r BZopp_0 BZsum_0r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)