proposition: Lemma wtl_div : forall n (w : word (S (S (S n)))), wordToNat (wtl (wtl (wtl w))) = NPeano.div (wordToNat w) 8.
proof: Proof. intros. pose proof (shatter_word_S w); destruct_ex; subst. pose proof (shatter_word_S x0); destruct_ex; subst. pose proof (shatter_word_S x2); destruct_ex; subst. simpl wtl. rewrite <- (NPeano.Nat.div_div _ 2 4) by omega. rewrite <- (NPeano.Nat.div_div _ 2 2) by omega. rewrite <- !NPeano.Nat.div2_div. rewrite !div2_WS. reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.Arith.Mult Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.DecideableEnsembles Fiat.Common.IterateBoundedIndex Fiat.Common.Tactics.CacheStringConstant Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.Core Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Automation.Solver 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.DomainNameOpt Fiat.Narcissus.Examples.DNS.DNSPacket Bedrock.Word