proposition: Lemma checksum'_app : forall bs1 bs2, checksum' (bs1 ++ bs2) = checksum' (bs2 ++ bs1).
proof: Proof. intros; apply checksum'_permutation, Permutation_app_comm. 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