proposition: Lemma BZlcm_nz a b: intp a -> intp b -> a <> \0z -> b <> \0z -> BZlcm a b <> \0z.
proof: Proof. move=> az bz ane bnz. move: (BZp_sBZ(ZpS_gcd az bz)) => gz. move: (BZlcm_prop1 az bz). set u := (a %/z BZgcd a b); move => [h _ _]; rewrite h. apply:(BZprod_nz (ZS_quo az gz) bz _ bnz) => h1. by move: (proj1(BZgcd_div az bz)); rewrite h1 BZprod_0r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)