proposition: Lemma mulzN (m n : int) : (m * (- n))%Z = - (m * n)%Z.
proof: Proof. by case: (intP m)=> {m} [|m|m]; rewrite ?mul0z //; case: (intP n)=> {n} [|n|n]; rewrite ?mulz0 //= mulnC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)