proposition: Lemma add_bytes_into_checksum_swap: forall (chk : W16) (b11 b12 b21 b22 : word 8), add_bytes_into_checksum b22 b21 (add_bytes_into_checksum b12 b11 chk) = add_bytes_into_checksum b12 b11 (add_bytes_into_checksum b22 b21 chk).
proof: Proof. unfold add_bytes_into_checksum, add_w16_into_checksum. intros; rewrite <- !OneC_plus_assoc. rewrite (OneC_plus_comm (combine b11 b12)). 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