proposition: Lemma mulNz (m n : int) : ((- m) * n)%Z = - (m * n)%Z.
proof: Proof. by rewrite mulzC mulzN mulzC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)