fact: Definition Z_of_int (n : int) : Z := match n with | Posz n => Z.of_nat n | Negz n' => Z.opp (Z.of_nat (n' + 1)) end.
imports: Coq(ZArith) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop finset prime) mathcomp(order binomial ssralg countalg ssrnum ssrint) mathcomp(zify_ssreflect)