diff options
| author |  Raphaël Monat <raphael.monat@ens-lyon.org> | 2017-10-08 21:17:00 +0200 |
|---|---|---|
| committer | Raphaël Monat <raphael.monat@ens-lyon.org> | 2017-10-08 21:17:00 +0200 |
| commit | 2ac3427a8366c28be37b33deb47e7823378263a3 (patch) | |
| tree | b8e556f84c2bcc2a5c43ecaa3cf76fd68def022c /theories | |
| parent | b4b778f1a1657e0b65f5ac3fe466ca9a1e8d55d3 (diff) | |
Removed leb_not_le (already existing as Nat.leb_nle)
Diffstat (limited to 'theories')
| -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}. |