proposition: Lemma N_below_pow2_nat {size} : forall (n: N), (n < FixInt.exp2 size)%N -> (N.to_nat n < (Word.pow2 size))%nat.
proof: Proof. intros. rewrite <- FixInt_exp2_Word_pow2_nat. auto using Nlt_out. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat CertifiedExtraction.Extraction.BinEncoders.Basics Coq.Lists.List Bedrock.Word Program Nomega