1 files changed, 16 insertions, 0 deletions
diff --git a/proofs/signatures/smt.plf b/proofs/signatures/smt.plf
index 06dc16153..57dc5bd1e 100644
--- a/proofs/signatures/smt.plf
+++ b/proofs/signatures/smt.plf
@@ -439,6 +439,22 @@
          (holds C))
     (holds (clc (neg v) C))))))))))
 
+;; Numeric primitives
+
+(program mpz_sub ((x mpz) (y mpz)) mpz
+	 (mp_add x (mp_mul (~1) y)))
+
+(program mp_ispos ((x mpz)) formula
+	 (mp_ifneg x false true))
+
+(program mpz_eq ((x mpz) (y mpz)) formula
+    (mp_ifzero (mpz_sub x y) true false))
+
+(program mpz_lt ((x mpz) (y mpz)) formula
+    (mp_ifneg (mpz_sub x y) true false))
+
+(program mpz_lte ((x mpz) (y mpz)) formula
+    (mp_ifneg (mpz_sub x y) true (mpz_eq x y)))
 
 ;; Example:
 ;;