proposition: Lemma lt_pow2_lognat k n : lognat k <= n -> k < 2^n.
proof: Proof. cbv [lognat]; intros H; destruct k; [pose proof Nat.pow_eq_0_iff 2 n; lia|]. enough (N.of_nat (S k) < N.of_nat (2^n))%N by lia; rewrite Nnat.Nat2N.inj_pow. rewrite !N.size_log2, Nnat.N2Nat.inj_succ in H by lia. apply N.log2_lt_pow2; lia. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith Permutation