add nat_thru_w64_id lemma

mjschwenne · Oct 27, 2024 · 4318c11 · 4318c11
1 parent 9911050
commit 4318c11
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/src/Helpers/Integers.v b/src/Helpers/Integers.v
@@ -691,3 +691,8 @@ Proof.
   { rewrite Z.mul_comm. apply ZLib.Z.Z_mod_mult'. }
   word.
 Qed.
+
+Lemma nat_thru_w64_id (x : nat) :
+  Z.of_nat x < 2^64 ->
+  uint.nat (W64 (Z.of_nat x)) = x.
+Proof. word. Qed.