proposition: Lemma FixInt_exp2_Word_Npow2 {size} : FixInt.exp2 size = Word.Npow2 size.
proof: Proof. induction size; simpl. + reflexivity. + unfold FixInt.exp2 in *; simpl. rewrite <- Pos_times_2_0, IHsize; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat CertifiedExtraction.Extraction.BinEncoders.Basics Coq.Lists.List Bedrock.Word Program