[changelog]: ≤-suc in Data.Nat.Properties

pmbittner · pmbittner · commit bbc81adf00c8 · 2025-07-01T11:22:03.000+02:00
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -254,6 +254,7 @@ Additions to existing modules
 * In `Data.Nat.Properties`:
   ```agda
   ∸-suc : n ≤ m → suc m ∸ n ≡ suc (m ∸ n)
+  ≤-suc : n ≤ m → n ≤ suc m
   ```
 
 * In `Data.Fin.Base`:
