proposition: Lemma lcmz_neq0 m n : (lcmz m n != 0) = (m != 0) && (n != 0).
proof: Proof. have [->|m_neq0] := eqVneq m 0; first by rewrite lcm0z. have [->|n_neq0] := eqVneq n 0; first by rewrite lcmz0. by rewrite gt_eqF// [0 < _]lcmn_gt0 !absz_gt0 m_neq0 n_neq0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime order) mathcomp(ssralg poly ssrnum ssrint archimedean rat matrix) mathcomp(polydiv perm zmodp mxalgebra vector)