proposition: Lemma build_aligned_ByteString_split : forall {n} (v : Vector.t _ n) {m} (v' : Vector.t _ m) b, build_aligned_ByteString v = ByteString_enqueue_ByteString b (build_aligned_ByteString v') -> exists v'' : Vector.t _ (n - m), b = build_aligned_ByteString v''.
proof: Proof. intros. assert (n = (n - m) + m). { rewrite plus_comm. eapply le_plus_minus. generalize (f_equal length_ByteString H); intros. unfold length_ByteString at 1 in H0; simpl in H0. replace (length_ByteString (ByteString_enqueue_ByteString b (build_aligned_ByteString v'))) with (length_ByteString b + (8 * m)) in H0. omega. rewrite <- (ByteStringToBoundedByteString_BoundedByteStringToByteString_eq b). rewrite <- (ByteStringToBoundedByteString_BoundedByteStringToByteString_eq (build_aligned_ByteString _)). rewrite ByteString_enqueue_ByteString_ByteStringToBoundedByteString. rewrite !length_ByteString_ByteStringToBoundedByteString_eq. rewrite ByteString_enqueue_ByteString_measure. unfold BoundedByteStringToByteString at 3. simpl. unfold Core.length_ByteString at 3; simpl. rewrite <- !ByteBuffer.to_list_length; omega. } revert v H; rewrite H0; intros; rewrite <- H0. rewrite (Vector_split_append v) in H. rewrite build_aligned_ByteString_append in H. eexists (fst (Vector_split (n - m) m v)). eapply ByteString_enqueue_ByteString_inj in H; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.NArith.NArith Coq.Arith.Arith Coq.Numbers.Natural.Peano.NPeano Coq.Logic.Eqdep_dec Fiat.Narcissus.Common.Specs Fiat.Narcissus.BinLib.Core Fiat.Narcissus.Formats.ByteBuffer Coq.Strings.String Coq.Vectors.Vector Fiat.Narcissus.Formats.WordOpt Fiat.Common.Equality