proposition: Lemma decode_word'_lt : forall (a : word (S sz)) (b' b1 : T), decode_word' _ b1 = Some (a, b') -> lt_B b' b1.
proof: Proof. simpl; intros; injections; unfold lt_B. destruct (dequeue_opt b1) as [ [? ?] | ] eqn: ? ; subst; simpl in *; try discriminate. apply measure_dequeue_Some in Heqo; subst. destruct (decode_word' sz t) as [ [? ?] | ] eqn: ? ; subst; simpl in *; try discriminate. eapply decode_word'_le in Heqo0; injections. rewrite Heqo. unfold le_B in *. pose proof (B_measure_gt_0 b). 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