proposition: Lemma build_aligned_ByteString_eq_split' : forall n sz v, (n <= sz)%nat -> build_aligned_ByteString v = build_aligned_ByteString (Guarded_Vector_split n sz v).
proof: Proof. intros; eapply ByteString_f_equal; simpl. instantiate (1 := eq_refl _); reflexivity. instantiate (1 := (le_plus_minus_r _ _ H)). generalize (le_plus_minus_r n sz H); clear. revert sz v; induction n; simpl; intros. unfold Guarded_Vector_split. rewrite <- Equality.transport_pp. generalize (eq_trans (minus_n_O sz) e); clear; intro. apply Eqdep_dec.eq_rect_eq_dec; auto with arith. destruct v; simpl in *. omega. unfold Guarded_Vector_split; fold Guarded_Vector_split; simpl. unfold ByteBuffer.t; erewrite eq_rect_Vector_cons; eauto. f_equal. apply IHn. Unshelve. omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Strings.String Coq.Arith.Mult Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.AlignedEncodeMonad Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedString Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.StringOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.DomainNameOpt Fiat.Common.IterateBoundedIndex Fiat.Common.Tactics.CacheStringConstant Fiat.Narcissus.Formats.IPChecksum Fiat.Narcissus.Common.ComposeCheckSum Bedrock.Word