proposition: Lemma mulrz_neq0 x n : x *~ n != 0 = ((n != 0) && (x != 0)).
proof: Proof. by rewrite mulrz_eq0 negb_or. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)