proposition: Lemma lt_B_trans : forall b (b1 : {b' : B | le_B b' b}) (b3 : {b' : B | lt_B b' (` b1)}), lt_B (` b3) b.
proof: Proof. intros; destruct b1; destruct b3; simpl in *. unfold le_B, lt_B in *; 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