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

Author: pmbittner

CHANGELOG.md

@@ -251,6 +251,11 @@ Additions to existing modules
   ∙-cong-∣ : x ∣ y → a ∣ b → x ∙ a ∣ y ∙ b
   ```
 
+* In `Data.Nat.Properties`:
+  ```agda
+  ∸-suc : m ≤ n → suc n ∸ m ≡ suc (n ∸ m)
+  ```
+
 * In `Data.Fin.Base`:
   ```agda
   _≰_ : Rel (Fin n) 0ℓ