From a6f0f03dcf002921f9f1b42a65bc023c4f6f4a84 Mon Sep 17 00:00:00 2001
From: fredokun <frederic.peschanski@lip6.fr>
Date: Wed, 29 Nov 2017 17:22:45 +0100
Subject: proposed fix for issue #3213: extra variable m in Lt.S_pred

---
 theories/Arith/Lt.v | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'theories')

diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index 035c4e466..2c2bea4a6 100644
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -107,6 +107,11 @@ Proof.
  intros. symmetry. now apply Nat.lt_succ_pred with m.
 Qed.
 
+Lemma S_pred_pos n: O < n -> n = S (pred n).
+Proof.
+ apply S_pred.
+Qed.
+
 Lemma lt_pred n m : S n < m -> n < pred m.
 Proof.
  apply Nat.lt_succ_lt_pred.
-- 
cgit v1.2.3