From b4b778f1a1657e0b65f5ac3fe466ca9a1e8d55d3 Mon Sep 17 00:00:00 2001
From: Raphaël Monat <raphael.monat@ens-lyon.org>
Date: Tue, 3 Oct 2017 20:45:13 +0200
Subject: Changed the statement of leb_not_le; shortened the proof

---
 theories/Arith/PeanoNat.v | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

(limited to 'theories')

diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v
index ffa56a6c3..95fd4cf86 100644
--- a/theories/Arith/PeanoNat.v
+++ b/theories/Arith/PeanoNat.v
@@ -172,15 +172,9 @@ Proof.
  apply leb_le.
 Qed.
 
-
-Lemma leb_not_le n m : (n <=? m) = false -> n > m.
+Lemma leb_not_le n m : (n <=? m) = false <-> ~n <= m.
 Proof.
-  revert m; induction n; destruct m; simpl; intros H_nm.
-  - congruence.
-  - congruence.
-  - apply lt_succ_r, le_0_n.
-  - specialize (IHn _ H_nm).
-    now apply lt_succ_r in IHn.
+  now rewrite <- leb_le, <- not_true_iff_false.
 Qed.
 
 (** ** Decidability of equality over [nat]. *)
-- 
cgit v1.2.3