fact: Definition charToBYTE (c: ascii) : BYTE := let (a0,a1,a2,a3,a4,a5,a6,a7) := c in [tuple a0;a1;a2;a3;a4;a5;a6;a7].
imports: Coq(ZArith.ZArith Strings.String) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp)