proposition: Lemma BtoW_BoundedNat8ToByte_natToWord : forall w, BtoW (BoundedNat8ToByte w) = natToWord 32 (` w).
proof: Proof. intros; apply wordToN_inj. unfold BoundedNat8ToByte, BtoW, zext. rewrite (InternetChecksum.wordToN_extend 8 24). destruct w as (? & pr); rewrite !IL.natToWordToN. - reflexivity. - simpl; apply BoundedN_BoundedNat in pr; etransitivity; eauto; reflexivity. - apply BoundedN_BoundedNat; assumption. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat CertifiedExtraction.Extraction.BinEncoders.Basics Coq.Lists.List Bedrock.Word Program Nomega