proposition: Lemma bvToNat_natToBv_inverse : forall n k, n >= lognat k -> bvToNat (natToBv n k) = k.
proof: Proof. intros; rewrite bvToNat_natToBv, Nat.mod_small; auto using lt_pow2_lognat. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith Permutation