proposition: Lemma wordToN_bound {size} (w: Word.word size): (wordToN w < FixInt.exp2 size)%N.
proof: Proof. dependent induction w; simpl. + reflexivity. + destruct b, (wordToN w); simpl; auto using FixInt_exp2_S_lt, FixInt_exp2_S_lt_strong. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat CertifiedExtraction.Extraction.BinEncoders.Basics Coq.Lists.List Bedrock.Word Program