fact: Definition toNat {n} (p: BITS n) := foldr (fun (b:bool) n => b + n.*2) 0 p.
imports: Coq(ZArith.ZArith Strings.String) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp)