proposition: Lemma checksum_app : forall bs1 bs2, (exists x, length bs1 = 2 * x)%nat -> (exists x, length bs2 = 2 * x)%nat -> checksum (bs1 ++ bs2) = checksum (bs2 ++ bs1).
proof: Proof. intros; rewrite !checksum_checksum'. rewrite !make_pairs_app by assumption. apply checksum'_app. 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