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

Author: pmbittner

src/Data/Nat/Properties.agda

@@ -1520,6 +1520,10 @@ pred[m∸n]≡m∸[1+n] (suc m) (suc n) = pred[m∸n]≡m∸[1+n] m n
 ------------------------------------------------------------------------
 -- Properties of _∸_ and _≤_/_<_
 
+∸-suc : m ≤ n → suc n ∸ m ≡ suc (n ∸ m)
+∸-suc z≤n       = refl
+∸-suc (s≤s m≤n) = ∸-suc m≤n
+
 m∸n≤m : ∀ m n → m ∸ n ≤ m
 m∸n≤m n       zero    = ≤-refl
 m∸n≤m zero    (suc n) = ≤-refl