fact: Definition BZ_of_Z (n:int) := match n with | Posz p => BZ_of_nat (nat_to_B p) | Negz p => BZm_of_nat (nat_to_B p.+1) end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype order) mathcomp(ssrnat ssrint ssralg ssrnum div)