fact: Definition oppz m := match m with | Posz n => if n is (n'.+1)%N then Negz n' else Posz 0 | Negz n => Posz (n.+1)%N end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)