proposition: Lemma FixInt_exp2_S_lt_strong: forall (n : nat) (p : positive), (N.pos p < FixInt.exp2 n)%N -> (N.pos p~1 < FixInt.exp2 (S n))%N.
proof: Proof. unfold FixInt.exp2; simpl; intros. rewrite <- (Pos_times_2_1 p). rewrite <- (Pos_times_2_0 (FixInt.exp2' _)). auto using N.double_above. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat CertifiedExtraction.Extraction.BinEncoders.Basics Coq.Lists.List Bedrock.Word Program