proposition: Lemma ascii_decode_lt : forall (b3 : B) (cd0 : CacheDecode) (a : ascii) (b' : B) (cd' : CacheDecode), decode_ascii b3 cd0 = Some (a, b', cd') -> lt_B b' b3.
proof: Proof. unfold decode_ascii; intros. destruct (WordOpt.decode_word b3 cd0) as [ [ [? ?] ?] | ] eqn: ? ; simpl in *; try discriminate. apply WordOpt.decode_word_lt in Heqo. injections; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.Narcissus.Common.Specs Fiat.Narcissus.BaseFormats Fiat.Narcissus.Formats.WordOpt Bedrock.Word Coq.ZArith.ZArith Coq.Strings.Ascii Coq.Numbers.BinNums Coq.NArith.BinNat