proposition: Lemma checksum'_permutation : forall bs1 bs2, Permutation bs1 bs2 -> checksum' bs1 = checksum' bs2.
proof: Proof. induction 1. - reflexivity. - simpl; rewrite IHPermutation; reflexivity. - simpl. rewrite add_bytes_into_checksum_swap; reflexivity. - etransitivity; eauto. 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