proposition: Lemma build_aligned_ByteString_eq_split : forall m n b H0, (m <= n)%nat -> build_aligned_ByteString b = (build_aligned_ByteString (eq_rect (m + (n - m)) (t (word 8)) (Guarded_Vector_split m n b) n H0)).
proof: Proof. intros. intros; eapply ByteString_f_equal; simpl. instantiate (1 := eq_refl _); reflexivity. instantiate (1 := eq_refl _). simpl. revert n b H0 H; induction m; simpl. intros ? ?; generalize (minus_n_O n). intros; rewrite <- Equality.transport_pp. apply Eqdep_dec.eq_rect_eq_dec; auto with arith. intros. inversion H; subst. - revert b H0 IHm; clear. intro; pattern m, b; apply Vector.caseS; simpl; intros. assert ((n + (n - n)) = n) by omega. rewrite eq_rect_Vector_cons with (H' := H). f_equal. erewrite <- IHm; eauto. - revert b H0 IHm H1; clear. intro; pattern m0, b; apply Vector.caseS; simpl; intros. assert ((m + (n - m)) = n) by omega. erewrite eq_rect_Vector_cons with (H' := H). f_equal. erewrite <- IHm; eauto. 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