diff --git a/prelude/cf/int.lp b/prelude/cf/int.lp
new file mode 100644
index 0000000000000000000000000000000000000000..7c07f856fb841d6b1bdc1dfb776a5a7a6f13bce5
--- /dev/null
+++ b/prelude/cf/int.lp
@@ -0,0 +1,10 @@
+require open encodings.cf prelude.cf.booleans prelude.cf.notequal
+
+constant symbol integer : Term uType
+definition int ≔ integer
+
+// Should be inherited
+symbol z : Term integer
+
+definition nonzero_integer ≔ psub integer (λ x: Term integer, neq z x)
+definition nzint ≔ nonzero_integer