fact: Definition toNegZ {n} (p: BITS n) := foldr (fun b z => if b then Z.double z else Z.succ (Z.double z)) Z0 p.
imports: Coq(ZArith.ZArith Strings.String) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp)