From 5fabef11c22080f1ba47ba7af7e369e304079cdc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Tue, 20 Aug 2019 17:30:20 +0200
Subject: [PATCH] add [n + k <= m => n <= m] helper lemma
---
util/nat.v | 11 +++++++++++
1 file changed, 11 insertions(+)
diff --git a/util/nat.v b/util/nat.v
index 59f5a6470..9845588f3 100644
--- a/util/nat.v
+++ b/util/nat.v
@@ -118,6 +118,17 @@ Section NatLemmas.
intros* AC. ssromega.
Qed.
+ (* We can drop additive terms on the lesser side of an inequality. *)
+ Lemma leq_addk:
+ forall m n k,
+ n + k <= m ->
+ n <= m.
+ Proof.
+ move=> m n p.
+ apply leq_trans.
+ by apply leq_addr.
+ Qed.
+
End NatLemmas.
Section Interval.
--
GitLab