proposition: Lemma mulZ_eq0 x y : (x * y == 0) = ((x == 0) || (y == 0)).
proof: Proof. apply/idP/idP => [/eqP/Zmult_integral[] ->| ]; try by rewrite eqxx // orbC. by case/orP => /eqP ->; rewrite ?mulZ0 ?mul0Z. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) ZArith Lia