[ add ] ∸-suc lemma for natural numbers (#2757)

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

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

* [refactor]: use ∸-suc instead of +-∸-assoc 1

* [refactor]: +-∸-assoc as proposed by jamesmckinna

* Update src/Data/Nat/Properties.agda

whitespace

* [refactor]: replace usages of +-∸-assoc 1 with ∸-suc

---------

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>

Author: pmbittner

CHANGELOG.md

@@ -17,6 +17,15 @@ Non-backwards compatible changes
 Minor improvements
 ------------------
 
+* Refactored usages of `+-∸-assoc 1` to `∸-suc` in:
+  ```agda
+  README.Data.Fin.Relation.Unary.Top
+  Algebra.Properties.Semiring.Binomial
+  Data.Fin.Subset.Properties
+  Data.Nat.Binary.Subtraction
+  Data.Nat.Combinatorics
+  ```
+
 Deprecated modules
 ------------------
 
@@ -28,3 +37,9 @@ New modules
 
 Additions to existing modules
 -----------------------------
+
+* In `Data.Nat.Properties`:
+  ```agda
+  ∸-suc : m ≤ n → suc n ∸ m ≡ suc (n ∸ m)
+  ```
+

doc/README/Data/Fin/Relation/Unary/Top.agda

@@ -17,7 +17,7 @@
 module README.Data.Fin.Relation.Unary.Top where
 
 open import Data.Nat.Base using (ℕ; zero; suc; _∸_; _≤_)
-open import Data.Nat.Properties using (n∸n≡0; +-∸-assoc; ≤-reflexive)
+open import Data.Nat.Properties using (n∸n≡0; ∸-suc; ≤-reflexive)
 open import Data.Fin.Base using (Fin; zero; suc; toℕ; fromℕ; inject₁; _>_)
 open import Data.Fin.Properties using (toℕ-fromℕ; toℕ<n; toℕ-inject₁)
 open import Data.Fin.Induction hiding (>-weakInduction)
@@ -76,7 +76,7 @@ opposite-prop {suc n} i with view i
 ... | ‵fromℕ  rewrite toℕ-fromℕ n | n∸n≡0 n = refl
 ... | ‵inject₁ j = begin
   suc (toℕ (opposite j)) ≡⟨ cong suc (opposite-prop j) ⟩
-  suc (n ∸ suc (toℕ j))  ≡⟨ +-∸-assoc 1 (toℕ<n j) ⟨
+  suc (n ∸ suc (toℕ j))  ≡⟨ ∸-suc (toℕ<n j) ⟨
   n ∸ toℕ j              ≡⟨ cong (n ∸_) (toℕ-inject₁ j) ⟨
   n ∸ toℕ (inject₁ j)    ∎ where open ≡-Reasoning
 

src/Algebra/Properties/Semiring/Binomial.agda

@@ -21,7 +21,7 @@ open import Data.Nat.Base as ℕ hiding (_+_; _*_; _^_)
 open import Data.Nat.Combinatorics
   using (_C_; nCn≡1; nC1≡n; nCk+nC[k+1]≡[n+1]C[k+1])
 open import Data.Nat.Properties as ℕ
-  using (<⇒<ᵇ; n<1+n; n∸n≡0; +-∸-assoc)
+  using (<⇒<ᵇ; n<1+n; n∸n≡0; ∸-suc)
 open import Data.Fin.Base as Fin
   using (Fin; zero; suc; toℕ; fromℕ; inject₁)
 open import Data.Fin.Patterns using (0F)
@@ -149,7 +149,7 @@ y*lemma x*y≈y*x {n} j = begin
     k≡j = toℕ-inject₁ j
 
     [n-k]≡[n-j] : [n-k] ≡ [n-j]
-    [n-k]≡[n-j] = ≡.trans (cong (n ∸_) k≡j) (+-∸-assoc 1 (toℕ<n j))
+    [n-k]≡[n-j] = ≡.trans (cong (n ∸_) k≡j) (∸-suc (toℕ<n j))
 
 ------------------------------------------------------------------------
 -- Now, a lemma characterising the sum of the term₁ and term₂ expressions

src/Data/Fin/Subset/Properties.agda

@@ -367,7 +367,7 @@ p∪∁p≡⊤ (inside  ∷ p) = cong (inside ∷_) (p∪∁p≡⊤ p)
 ∣∁p∣≡n∸∣p∣ (inside  ∷ p) = ∣∁p∣≡n∸∣p∣ p
 ∣∁p∣≡n∸∣p∣ (outside ∷ p) = begin
   suc ∣ ∁ p ∣     ≡⟨ cong suc (∣∁p∣≡n∸∣p∣ p) ⟩
-  suc (_ ∸ ∣ p ∣) ≡⟨ sym (ℕ.+-∸-assoc 1 (∣p∣≤n p)) ⟩
+  suc (_ ∸ ∣ p ∣) ≡⟨ sym (ℕ.∸-suc (∣p∣≤n p)) ⟩
   suc  _ ∸ ∣ p ∣  ∎
   where open ≡-Reasoning
 

src/Data/Nat/Binary/Subtraction.agda

@@ -88,7 +88,7 @@ toℕ-homo-∸ 2[1+ x ] 1+[2 y ] with x <? y
 ... | no  x≮y  = begin
   ℕ.suc (2 ℕ.* toℕ (x ∸ y))                     ≡⟨ cong (ℕ.suc ∘ (2 ℕ.*_)) (toℕ-homo-∸ x y) ⟩
   ℕ.suc (2 ℕ.* (toℕ x ℕ.∸ toℕ y))               ≡⟨ cong ℕ.suc (ℕ.*-distribˡ-∸ 2 (toℕ x) (toℕ y)) ⟩
-  ℕ.suc (2 ℕ.* toℕ x ℕ.∸ 2 ℕ.* toℕ y)           ≡⟨ sym (ℕ.+-∸-assoc 1 (ℕ.*-monoʳ-≤ 2 (toℕ-mono-≤ (≮⇒≥ x≮y)))) ⟩
+  ℕ.suc (2 ℕ.* toℕ x ℕ.∸ 2 ℕ.* toℕ y)           ≡⟨ sym (ℕ.∸-suc (ℕ.*-monoʳ-≤ 2 (toℕ-mono-≤ (≮⇒≥ x≮y)))) ⟩
   ℕ.suc (2 ℕ.* toℕ x) ℕ.∸ 2 ℕ.* toℕ y           ≡⟨ sym (cong (ℕ._∸ 2 ℕ.* toℕ y) (ℕ.+-suc (toℕ x) (1 ℕ.* toℕ x))) ⟩
   2 ℕ.* (ℕ.suc (toℕ x)) ℕ.∸ ℕ.suc (2 ℕ.* toℕ y) ∎
   where open ≡-Reasoning

src/Data/Nat/Combinatorics.agda

@@ -122,7 +122,7 @@ module _ {n k} (k<n : k < n) where
     [n-k-1]!         = [n-k-1] !
 
     [n-k]≡1+[n-k-1]  : [n-k] ≡ suc [n-k-1]
-    [n-k]≡1+[n-k-1]  = +-∸-assoc 1 k<n
+    [n-k]≡1+[n-k-1]  = ∸-suc k<n
 
 
   [n-k]*[n-k-1]!≡[n-k]! : [n-k] * [n-k-1]! ≡ [n-k]!

src/Data/Nat/Properties.agda

@@ -1524,6 +1524,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
@@ -1614,12 +1618,11 @@ m≤n⇒n∸m≤n (s≤s m≤n) = m≤n⇒m≤1+n (m≤n⇒n∸m≤n m≤n)
 ∸-+-assoc (suc m) (suc n) o = ∸-+-assoc m n o
 
 +-∸-assoc : ∀ m {n o} → o ≤ n → (m + n) ∸ o ≡ m + (n ∸ o)
-+-∸-assoc m (z≤n {n = n})             = begin-equality m + n ∎
-+-∸-assoc m (s≤s {m = o} {n = n} o≤n) = begin-equality
-  (m + suc n) ∸ suc o  ≡⟨ cong (_∸ suc o) (+-suc m n) ⟩
-  suc (m + n) ∸ suc o  ≡⟨⟩
-  (m + n) ∸ o          ≡⟨ +-∸-assoc m o≤n ⟩
-  m + (n ∸ o)          ∎
++-∸-assoc zero    {n = n} {o = o} _   = begin-equality n ∸ o ∎
++-∸-assoc (suc m) {n = n} {o = o} o≤n = begin-equality
+  suc (m + n) ∸ o   ≡⟨ ∸-suc (m≤n⇒m≤o+n m o≤n) ⟩
+  suc ((m + n) ∸ o) ≡⟨ cong suc (+-∸-assoc m o≤n) ⟩
+  suc (m + (n ∸ o)) ∎
 
 m≤n+o⇒m∸n≤o : ∀ m n {o} → m ≤ n + o → m ∸ n ≤ o
 m≤n+o⇒m∸n≤o      m  zero    le = le
@@ -1634,7 +1637,7 @@ m<n+o⇒m∸n<o (suc m) (suc n)             lt = m<n+o⇒m∸n<o m n  (s<s⁻¹
 m+n≤o⇒m≤o∸n : ∀ m {n o} → m + n ≤ o → m ≤ o ∸ n
 m+n≤o⇒m≤o∸n zero    le       = z≤n
 m+n≤o⇒m≤o∸n (suc m) (s≤s le)
-  rewrite +-∸-assoc 1 (m+n≤o⇒n≤o m le) = s≤s (m+n≤o⇒m≤o∸n m le)
+  rewrite ∸-suc (m+n≤o⇒n≤o m le) = s≤s (m+n≤o⇒m≤o∸n m le)
 
 m≤o∸n⇒m+n≤o : ∀ m {n o} (n≤o : n ≤ o) → m ≤ o ∸ n → m + n ≤ o
 m≤o∸n⇒m+n≤o m         z≤n       le rewrite +-identityʳ m = le
@@ -1671,7 +1674,7 @@ m∸n+n≡m {m} {n} n≤m = begin-equality
 m∸[m∸n]≡n : ∀ {m n} → n ≤ m → m ∸ (m ∸ n) ≡ n
 m∸[m∸n]≡n {m}     {_}     z≤n       = n∸n≡0 m
 m∸[m∸n]≡n {suc m} {suc n} (s≤s n≤m) = begin-equality
-  suc m ∸ (m ∸ n)   ≡⟨ +-∸-assoc 1 (m∸n≤m m n) ⟩
+  suc m ∸ (m ∸ n)   ≡⟨ ∸-suc (m∸n≤m m n) ⟩
   suc (m ∸ (m ∸ n)) ≡⟨ cong suc (m∸[m∸n]≡n n≤m) ⟩
   suc n             ∎