proposition: Lemma idomain_axiomz m n : m * n = 0 -> (m == 0) || (n == 0).
proof: Proof. by case: m n => m [] n //= /eqP; rewrite ?(NegzE, mulrN, mulNr) ?oppr_eq0 -PoszM [_ == _]muln_eq0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)