proposition: Lemma natToBv_bvToNat_inverse : forall n k, (natToBv n (bvToNat k)) = k.
proof: Proof. symmetry. induction k; cbn; trivial; f_equal. { rewrite Nat.odd_add_even by (exists (bvToNat k); cbv[Nat.double]; lia). symmetry; apply Nat.b2n_bit0. } rewrite Nat.div2_div, Nat.double_twice, Nat.add_b2n_double_div2; trivial. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith Permutation