proposition: Lemma Nat2pointerT_pf : forall n, natToWord 8 191 < natToWord 8 (NPeano.modulo (NPeano.div n 256) 64 + 192).
proof: Proof. intros; apply WordFacts.natToWord_wlt. - simpl; apply Nomega.Nlt_in; simpl; compute; omega. - apply Nomega.Nlt_in. apply Lt.lt_le_trans with (m := 64 + 192); [ rewrite Nnat.Nat2N.id | compute; omega]. apply Plus.plus_lt_compat_r. refine (proj2 (NPeano.mod_bound_pos _ _ _ _)); omega. - omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.Strings.Ascii Coq.Strings.String Coq.Logic.Eqdep_dec Fiat.Computation.Core Fiat.Computation.FixComp Fiat.Computation.Notations Fiat.Computation.Refinements.General Fiat.Common.DecideableEnsembles Fiat.Narcissus.Common.Specs Fiat.Narcissus.Formats.FixStringOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.AsciiOpt