proposition: Lemma FixInt_exp2_Word_pow2_nat {size} : N.to_nat (FixInt.exp2 size) = Word.pow2 size.
proof: Proof. rewrite FixInt_exp2_Word_pow2_N; apply Nat2N.id. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat CertifiedExtraction.Extraction.BinEncoders.Basics Coq.Lists.List Bedrock.Word Program