fact: Definition toZ {n} (bs: BITS n.+1) := match splitmsb bs with | (false, bs') => toPosZ bs' | (true, bs') => Z.opp (Z.succ (toNegZ bs')) end.
imports: Coq(ZArith.ZArith Strings.String) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp)