fact: Definition mulz (m n : int) := match m, n with | Posz m', Posz n' => (m' * n')%N%:Z | Negz m', Negz n' => (m'.+1%N * n'.+1%N)%N%:Z | Posz m', Negz n' => - (m' * (n'.+1%N))%N%:Z | Negz n', Posz m' => - (m' * (n'.+1%N))%N%:Z end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)