fact: Fixpoint fromBin s : BITS (length s) := if s is String c s then joinmsb (charToBit c, fromBin s) else #0.
imports: Coq(ZArith.ZArith Strings.String) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp)