proposition: Lemma lognat_monotonic : forall n1 n2, (n1 < n2 -> lognat n1 <= lognat n2)%nat.
proof: Proof. intros ? ? H. pose proof N.log2_le_mono (N.of_nat n1) (N.of_nat n2). case n1, n2; try (cbn; lia); cbv [lognat]; rewrite !N.size_log2; try lia. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith Permutation