proposition: Lemma ByteBuffer_checksum_bound_ok' : forall n {sz} (bytes :ByteBuffer.t sz) acc, Vector_checksum_bound n bytes acc = ByteBuffer_fold_left16 add_w16_into_checksum n bytes acc.
proof: Proof. fix IH 3. destruct bytes as [ | hd sz [ | hd' sz' tl ] ]; intros; simpl. - destruct n as [ | [ | ] ]; reflexivity. - destruct n as [ | [ | ] ]; reflexivity. - destruct n as [ | [ | ] ]; simpl; try reflexivity. rewrite IH; reflexivity. Qed.
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