proposition: Lemma n_eq_0_lt : forall n, n <> wzero 8 -> (0 < wordToNat n)%nat.
proof: Proof. induction n; unfold wzero; simpl. - congruence. - destruct b; simpl; try omega. intros. assert (n0 <> wzero n) by (intro; subst; apply H; f_equal). apply IHn in H0. 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