proposition: Lemma addPeekENone' : forall env n m, peekE env = Some m -> ~ lt (n + (pointerT2Nat m)) (pow2 14)%nat -> peekE (addE env (n * 8)) = None.
proof: Proof. simpl; intros; subst. destruct (fst env); simpl in *; try discriminate. injections. find_if_inside; try reflexivity. unfold If_Opt_Then_Else. rewrite !wtl_div in *. exfalso; apply H0. rewrite pointerT2Nat_Nat2pointerT in *; try (eapply pow2_div; eassumption). eapply (mult_lt_compat_l' _ _ 8); try omega. destruct n; try omega. exfalso; apply H0. simpl. eapply (mult_lt_compat_l' _ _ 8); try omega. - eapply le_lt_trans. apply NPeano.Nat.mul_div_le; omega. simpl in l. rewrite mult_pow2_8; simpl; omega. - rewrite mult_plus_distr_l. assert (8 <> 0) by omega. pose proof (NPeano.Nat.mul_div_le (wordToNat w) 8 H). apply le_lt_trans with (8 * S n + (wordToNat w)). omega. rewrite mult_pow2_8; simpl; omega. 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