fact: Definition ByteBuffer_fold_left16 {B} (f: word 16 -> B -> B) {sz: nat} n (v: ByteBuffer.t sz) acc := ByteBuffer_fold_left_pair (fun hi lo => f (combine lo hi)) n v acc (wzero _).
imports: Fiat.Common.Coq__8_4__8_5__Compat List Bedrock.Word Coq.ZArith.ZArith Coq.micromega.Psatz NArith NArithRing ZArith ZArithRing Program Coq.micromega.Psatz AlignedByteString Permutation