proposition: Lemma BZrem_div1 a b: intp a -> intp b -> b <> \0z -> (BZ_val a) %%c (BZ_val b) = \0c -> (a %%z b) = \0z.
proof: Proof. move => az bz bnz de; rewrite /BZrem {1} (BZquo_div1 az bz bnz de). exact: (BZdiff_diag (ZSp bz (ZS_quo az bz))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)