proposition: Lemma make_pairs_app {A} : forall bs1, (exists x, length bs1 = 2 * x)%nat -> (forall bs2 z, @make_pairs A (bs1 ++ bs2) z = make_pairs bs1 z ++ make_pairs bs2 z).
proof: Proof. fix IH 1. destruct bs1; simpl. - reflexivity. - destruct bs1; simpl; intros Hex *; destruct Hex as [x ?]. + omega. + f_equal; rewrite IH. * reflexivity. * exists (pred x); omega. 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