From d2bd7a4bccdbf13a9ef2010b09698a184f0a8893 Mon Sep 17 00:00:00 2001
From: Rob23oba <robin.arnez@web.de>
Date: Sun, 2 Nov 2025 09:32:59 +0100
Subject: [PATCH] simplify Nat.ble

---
 src/Init/Prelude.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index a8e4d1133878..ed83ab88ff72 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -1831,8 +1831,7 @@ Examples:
 -/
 @[extern "lean_nat_dec_le"]
 def Nat.ble : @& Nat → @& Nat → Bool
-  | zero,   zero   => true
-  | zero,   succ _ => true
+  | zero,   _      => true
   | succ _, zero   => false
   | succ n, succ m => ble n m