proposition: Lemma length_ByteString_IPChecksum_ByteAligned : forall b, NPeano.modulo (length_ByteString b) 16 = 0 -> IPChecksum_ByteAligned b.
proof: Proof. destruct b; unfold length_ByteString. unfold Core.padding, Core.byteString. intros; assert (padding = 0). rewrite NPeano.Nat.mod_mul_r with (b := 8) (c := 2) in H by eauto. apply Plus.plus_is_O in H; destruct H. apply Mult.mult_is_O in H0; destruct H0. congruence. rewrite Mult.mult_comm, NPeano.Nat.mod_add in H by eauto. destruct padding as [ | [ | [ | [ | [ | [ | [ | [ | [ ] ] ] ] ] ] ] ] ] ; eauto; simpl in H; try omega. unfold IPChecksum_ByteAligned; intuition eauto. subst; rewrite plus_O_n in H. eapply NPeano.Nat.mod_divides in H; eauto. destruct H. simpl. exists x. unfold AlignedByteString.numBytes in H. omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Strings.String Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.EnumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.Core Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.Common.ComposeCheckSum Fiat.Narcissus.Common.ComposeIf Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.Option Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Stores.EmptyStore Fiat.Narcissus.Formats.Bool Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.Vector Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.InternetChecksum Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.BaseFormats Bedrock.Word