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