fact: Fixpoint stringToTupleBYTE (s: string) : (length s).-tuple BYTE := if s is String c s then cons_tuple (charToBYTE c) (stringToTupleBYTE s) else nil_tuple _.
imports: Coq(ZArith.ZArith Strings.String) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp)