proposition: Lemma BZ_quorem00 b: intp b -> (\0z %%z b = \0z /\ \0z %/z b = \0z).
proof: Proof. move => bz. case: (equal_or_not b \0z); first by move => ->; apply: (BZ_quorem0 ZS0). move: ZS0 => zz bnz. have: \0z %/z b = \0z. rewrite /BZquo - lock / BZquo_int; Ytac0; rewrite BZ0_val. move: (cdivision_of_zero (BZ_valN bz)) => [[qa qb ->] ->]. by rewrite -/BZ_zero BZopp_0; Ytac0; Ytac0; Ytac0. move => h;split => //; rewrite /BZrem h BZprod_0r; apply: (BZdiff_diag zz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)