aboutsummaryrefslogtreecommitdiff
path: root/src/Util/ZUtil/Le.v
diff options
context:
space:
mode:
authorGravatar jadep <jadep@mit.edu>2019-03-12 15:30:56 -0400
committerGravatar jadephilipoom <jade.philipoom@gmail.com>2019-03-26 08:35:33 -0400
commita201b0a8e525cab5c3cb019ccd707b7367aa3ecc (patch)
treef53c6cdc31eb546681a5689af454f04281a9b9b6 /src/Util/ZUtil/Le.v
parent14bd0770e068e5669cdbc4a0135e4cb65b3dad94 (diff)
add some hints to the global databases
Diffstat (limited to 'src/Util/ZUtil/Le.v')
-rw-r--r--src/Util/ZUtil/Le.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/ZUtil/Le.v b/src/Util/ZUtil/Le.v
index a32d0fdd0..d49931818 100644
--- a/src/Util/ZUtil/Le.v
+++ b/src/Util/ZUtil/Le.v
@@ -61,4 +61,4 @@ Module Z.
Lemma le_add_1_iff x y : x + 1 <= y <-> x < y.
Proof. lia. Qed.
-End Z.
+End Z. \ No newline at end of file