proposition: Lemma BZlcm_zero a: intp a -> BZlcm a \0z = \0z.
proof: Proof. move => az; rewrite /BZlcm BZprod_0r. exact (proj2 (BZ_quorem00 (BZp_sBZ (ZpS_gcd az ZS0)))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)