proposition: Lemma Z_idomain_axiom : forall x y : Z, x * y = 0 -> (x == 0) || (y == 0).
proof: Proof. move=> x y; rewrite -[x * y]/(Zmult x y); move/Zmult_integral; case=> -> //=. by rewrite eqxx orbT. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrnat seq order) mathcomp(choice fintype finfun ssrfun bigop ssralg) Zbool Qcanon ZArith