From 2ac3427a8366c28be37b33deb47e7823378263a3 Mon Sep 17 00:00:00 2001 From: Raphaël Monat Date: Sun, 8 Oct 2017 21:17:00 +0200 Subject: Removed leb_not_le (already existing as Nat.leb_nle) --- theories/Arith/PeanoNat.v | 5 ----- 1 file changed, 5 deletions(-) (limited to 'theories') diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v index 95fd4cf86..bde6f1bb4 100644 --- a/theories/Arith/PeanoNat.v +++ b/theories/Arith/PeanoNat.v @@ -172,11 +172,6 @@ Proof. apply leb_le. Qed. -Lemma leb_not_le n m : (n <=? m) = false <-> ~n <= m. -Proof. - now rewrite <- leb_le, <- not_true_iff_false. -Qed. - (** ** Decidability of equality over [nat]. *) Lemma eq_dec : forall n m : nat, {n = m} + {n <> m}. -- cgit v1.2.3