proposition: Lemma bvToNat_natToBv : forall n k, bvToNat (natToBv n k) = k mod (2 ^ n).
proof: Proof. induction n; cbn [bvToNat natToBv]; trivial; intros. cbn [Nat.pow]; rewrite Nat.mod_mul_r by (try apply Nat.pow_nonzero; lia). setoid_rewrite Nat.bit0_mod. f_equal. rewrite IHn, Nat.div2_div, Nat.double_twice; trivial. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith Permutation