fact: Definition wordToN_bounded {size} (w: Word.word size) : { n | (n < FixInt.exp2 size)%N } := exist _ (wordToN w) (wordToN_bound w).
imports: Fiat.Common.Coq__8_4__8_5__Compat CertifiedExtraction.Extraction.BinEncoders.Basics Coq.Lists.List Bedrock.Word Program