From 3965e6bd0bc08679ac28aa600e86ca99a3255c5b Mon Sep 17 00:00:00 2001
From: mamonet <maamoun.tk@gmail.com>
Date: Wed, 16 Oct 2024 08:21:29 +0000
Subject: [PATCH] Restore neg_equiv_lemma

---
 .../fstar/rust_primitives/Rust_primitives.Integers.fsti       | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fsti b/proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fsti
index 4ae6402d1..25739a3dd 100644
--- a/proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fsti
+++ b/proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fsti
@@ -315,6 +315,10 @@ let abs_int (#t:inttype) (a:int_t t{minint t < v a}) =
 let neg (#t:inttype{signed t}) (a:int_t t{range (0 - v a) t}) =
     mk_int #t (0 - (v a))
 
+val neg_equiv_lemma: #t:inttype{signed t /\ not (I128? t)}
+  -> a:int_t t{range (0 - v a) t}
+  -> Lemma (neg a == sub #t (mk_int 0) a /\
+          (lognot a = sub (neg a) (mk_int 1)))
 
 ///
 /// Operators available for all machine integers