proposition: Lemma decode_word'_le : forall (a : word sz) (b' b1 : T), decode_word' _ b1 = Some (a, b') -> le_B b' b1.
proof: Proof. intros; apply decode_encode_word'_Some in H; subst. unfold le_B. rewrite mappend_measure; omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Common Fiat.Computation.Notations Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.BaseFormats