fact: Fixpoint checksum bytes : W16 := match bytes with | nil => wzero _ | x :: nil => add_bytes_into_checksum x (wzero _) (wzero _) | x :: y :: t => add_bytes_into_checksum x y (checksum t) end.
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