proposition: Lemma split2_split2 : forall n m o (w : word (n + (m + o))), split2' m o (split2' n (m + o) w) = split2' (n + m) o (eq_rect _ _ w _ (plus_assoc _ _ _)).
proof: Proof. induction n; simpl; intros. - rewrite <- Eqdep_dec.eq_rect_eq_dec; auto with arith. - rewrite IHn. f_equal. pose proof (shatter_word_S w); destruct_ex; subst. clear. rewrite <- WS_eq_rect_eq with (H := plus_assoc n m o). revert m o x0 x; induction n; simpl; intros. + rewrite <- !Eqdep_dec.eq_rect_eq_dec; eauto using Peano_dec.eq_nat_dec. + erewrite <- WS_eq_rect_eq; fold plus; pose proof (shatter_word_S x0); destruct_ex; subst; f_equal. rewrite IHn; f_equal. erewrite <- WS_eq_rect_eq; reflexivity. 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