proposition: Lemma bvToNat_natToBv_eq : forall n (v : Bvector n) k, bvToNat v = k -> v = natToBv n k.
proof: Proof. pose proof natToBv_bvToNat_inverse. congruence. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith Permutation