fact: Definition int_of_natsum (m : nat + nat) := match m with inl p => Posz p | inr n => Negz n end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)