fact: Definition checksum'' byte_pairs acc : W16 := fold_left (fun chk p => add_bytes_into_checksum (fst p) (snd p) chk) byte_pairs acc.
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