proposition: Lemma N_below_pow2_N {size} : forall (n: N), (n < FixInt.exp2 size)%N -> (n < N.of_nat (Word.pow2 size))%N.
proof: Proof. intros; rewrite <- FixInt_exp2_Word_pow2_N; assumption. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat CertifiedExtraction.Extraction.BinEncoders.Basics Coq.Lists.List Bedrock.Word Program