fact: Fixpoint bitsToBytes n : BITS (n*8) -> n.-tuple BYTE := if n is n'.+1 return BITS (n*8) -> n.-tuple BYTE then fun xs => let (hi,lo) := splitAtByte n' xs in cons_tuple lo (bitsToBytes _ hi) else fun xs => nil_tuple _.
imports: Coq(ZArith.ZArith Strings.String) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp)