diff options
| -rw-r--r-- | theories/Arith/PeanoNat.v | 5 |
1 files changed, 0 insertions, 5 deletions
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}. |