proposition: Lemma BZdvd_zero1 a: intp a -> (a %|z \0z /\ \0z %/z a = \0z).
proof: Proof. move => az; move: (BZ_quorem00 az) => [pa pb]. split => //; split => //; apply: ZS0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)