fact: Fixpoint fromPosZ {n} (z: Z): BITS n := if n is _.+1 then joinlsb (fromPosZ (Z.div2 z), negb (Zeven_bool z)) else nilB.
imports: Coq(ZArith.ZArith Strings.String) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp)