proposition: Fact poly_idomainAxiom p q : p * q = 0 -> (p == 0) || (q == 0).
proof: Proof. move=> pq0; apply/norP=> [[p_nz q_nz]]; move/eqP: (size_mul p_nz q_nz). by rewrite eq_sym pq0 size_poly0 (polySpred p_nz) (polySpred q_nz) addnS. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)