diff --git a/util/epsilon.v b/util/epsilon.v
new file mode 100644
index 0000000000000000000000000000000000000000..d66c6b81f9ca62cb9c4a46f54a6657b845572648
--- /dev/null
+++ b/util/epsilon.v
@@ -0,0 +1,6 @@
+Module Epsilon.
+
+  (* ε is defined as the smallest positive number. *)
+  Definition ε := 1.
+
+End Epsilon.
\ No newline at end of file