fixed merge commit; lifted out lemmas; tweaked

Author: jamesmckinna

CHANGELOG.md

@@ -2069,8 +2069,6 @@ Other minor changes
   <-step        : m < n → m < 1 + n
   m<1+n⇒m<n∨m≡n : m < suc n → m < n ⊎ m ≡ n
 
-  n<ᵇ1+n : ∀ n → (n <ᵇ suc n) ≡ true
-
   z<′s : zero <′ suc n
   s<′s : m <′ n → suc m <′ suc n
   <⇒<′ : m < n → m <′ n
@@ -2121,7 +2119,9 @@ Other minor changes
 
 * Added new proofs in `Data.Nat.Combinatorics`:
   ```agda
-  k![n∸k]!∣n!              : k ≤ n →  k ! * (n ∸ k) ! ∣ n !
+  [n-k]*[n-k-1]!≡[n-k]!   : k < n → (n ∸ k) * (n ∸ suc k) ! ≡ (n ∸ k) !
+  [n-k]*d[k+1]≡[k+1]*d[k] : k < n → (n ∸ k) * ((suc k) ! * (n ∸ suc k) !) ≡ (suc k) * (k ! * (n ∸ k) !)
+  k![n∸k]!∣n!              : k ≤ n → k ! * (n ∸ k) ! ∣ n !
   nP1≡n                   : n P 1 ≡ n
   nC1≡n                   : n C 1 ≡ n
   nCk+nC[k+1]≡[n+1]C[k+1] : n C k + n C (suc k) ≡ suc n C suc k

src/Data/Nat/Combinatorics.agda

@@ -12,7 +12,7 @@ open import Data.Nat.Base
 open import Data.Nat.DivMod
 open import Data.Nat.Divisibility
 open import Data.Nat.Properties
-open import Relation.Binary.Definitions
+open import Relation.Binary.Definitions 
 open import Relation.Binary.PropositionalEquality
   using (_≡_; refl; sym; cong; subst)
 
@@ -49,11 +49,11 @@ nPn≡n! n = begin-equality
     _ = (n ∸ n) !≢0
 
 nP1≡n : ∀ n → n P 1 ≡ n
-nP1≡n zero    = k>n⇒nPk≡0 (z<s {n = zero})
+nP1≡n zero        = refl
 nP1≡n n@(suc n-1) = begin-equality
-  n P 1        ≡⟨ nPk≡n!/[n∸k]! (s≤s (z≤n {n-1})) ⟩
-  n ! / n-1 !  ≡⟨ m*n/n≡m n (n-1 !) ⟩
-  n            ∎
+  n P 1          ≡⟨ nPk≡n!/[n∸k]! (s≤s (z≤n {n-1})) ⟩
+  n ! / n-1 !    ≡⟨ m*n/n≡m n (n-1 !) ⟩
+  n              ∎
   where instance
     _ = n-1 !≢0
 
@@ -109,7 +109,51 @@ nC1≡n n@(suc n-1) = begin-equality
 ------------------------------------------------------------------------
 -- Arithmetic of (n C k)
 
-k![n∸k]!∣n! : ∀ {n k} → k ≤ n →  k ! * (n ∸ k) ! ∣ n !
+module _ {n k} (k<n : k < n) where
+
+  private
+
+    [n-k]            = n ∸ k
+    [n-k-1]          = n ∸ suc k
+
+    [n-k]!           = [n-k] !
+    [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]*[n-k-1]!≡[n-k]! : [n-k] * [n-k-1]! ≡ [n-k]!
+  [n-k]*[n-k-1]!≡[n-k]! = begin-equality
+      [n-k] * [n-k-1]!
+        ≡⟨ cong (_* [n-k-1]!) [n-k]≡1+[n-k-1] ⟩
+      (suc [n-k-1]) * [n-k-1]!
+        ≡˘⟨ cong _! [n-k]≡1+[n-k-1] ⟩
+      [n-k]!                ∎
+
+  private
+
+    n!           = n !
+    k!           = k !
+    [k+1]!       = (suc k) !
+
+    d[k]         = k! * [n-k]!
+    [k+1]*d[k]   = (suc k) * d[k]
+    d[k+1]       = [k+1]! * [n-k-1]!
+    [n-k]*d[k+1] = [n-k] * d[k+1]
+
+  [n-k]*d[k+1]≡[k+1]*d[k] : [n-k]*d[k+1] ≡ [k+1]*d[k]
+  [n-k]*d[k+1]≡[k+1]*d[k] = begin-equality
+    [n-k]*d[k+1]
+      ≡⟨ x∙yz≈y∙xz [n-k] [k+1]! [n-k-1]! ⟩
+    [k+1]! * ([n-k] * [n-k-1]!)
+      ≡⟨ *-assoc (suc k) k! ([n-k] * [n-k-1]!) ⟩
+    (suc k) * (k! * ([n-k] * [n-k-1]!))
+       ≡⟨ cong ((suc k) *_) (cong (k! *_) [n-k]*[n-k-1]!≡[n-k]!) ⟩
+    [k+1]*d[k]             ∎
+    where open CommSemigroupProperties *-commutativeSemigroup
+
+k![n∸k]!∣n! : ∀ {n k} → k ≤ n → k ! * (n ∸ k) ! ∣ n !
 k![n∸k]!∣n! {n} {k} k≤n = subst (_∣ n !) (*-comm ((n ∸ k) !) (k !)) ([n∸k]!k!∣n! k≤n)
 
 nCk+nC[k+1]≡[n+1]C[k+1] : ∀ n k → n C k + n C (suc k) ≡ suc n C suc k
@@ -139,7 +183,7 @@ nCk+nC[k+1]≡[n+1]C[k+1] n k with <-cmp k n
   n! / d[k] + _
     ≡˘⟨ cong (_+ [n-k]*n!/[n-k]*d[k+1]) (m*n/m*o≡n/o (suc k) n! d[k]) ⟩
   (suc k * n!) / [k+1]*d[k] + _
-    ≡⟨ cong (((suc k * n!) / [k+1]*d[k]) +_) (/-congʳ [n-k]*d[k+1]≡[k+1]*d[k]) ⟩
+    ≡⟨ cong (((suc k * n!) / [k+1]*d[k]) +_) (/-congʳ ([n-k]*d[k+1]≡[k+1]*d[k] k<n)) ⟩
   (suc k * n!) / [k+1]*d[k] + ((n ∸ k) * n! / [k+1]*d[k])
     ≡˘⟨ +-distrib-/-∣ˡ _ (*-monoʳ-∣ (suc k) (k![n∸k]!∣n! k≤n)) ⟩
   ((suc k) * n! + (n ∸ k) * n!) / [k+1]*d[k]
@@ -166,48 +210,24 @@ nCk+nC[k+1]≡[n+1]C[k+1] n k with <-cmp k n
     [n-k]                   = n ∸ k
     [n-k-1]                 = n ∸ suc k
 
-    [n-k-1]+1≡[n-k]         : suc [n-k-1] ≡ [n-k]
-    [n-k-1]+1≡[n-k]         = [m-n-1]+1≡[m-n] k<n
-
     n!                      = n !
     k!                      = k !
     [k+1]!                  = (suc k) !
     [n-k]!                  = [n-k] !
     [n-k-1]!                = [n-k-1] !
 
-    [n-k]*[n-k-1]!≡[n-k]!   : [n-k] * [n-k-1]! ≡ [n-k]!
-    [n-k]*[n-k-1]!≡[n-k]!   = begin-equality
-      [n-k] * [n-k-1]!
-        ≡˘⟨ cong (_* [n-k-1]!) [n-k-1]+1≡[n-k] ⟩
-      (suc [n-k-1]) * [n-k-1]!
-        ≡⟨ cong _! [n-k-1]+1≡[n-k] ⟩
-      [n-k]!                ∎
-
     d[k]                    = k! * [n-k]!
     [k+1]*d[k]              = (suc k) * d[k]
     d[k+1]                  = [k+1]! * [n-k-1]!
-    [n-k]*d[k]              = [n-k] * d[k]
     [n-k]*d[k+1]            = [n-k] * d[k+1]
     n!/[n-k]*d[k+1]         = n ! / [n-k]*d[k+1]
     [n-k]*n!/[n-k]*d[k+1]   = [n-k] * n! / [n-k]*d[k+1]
     [n-k]*n!/[k+1]*d[k]     = [n-k] * n! / [k+1]*d[k]
 
-    [n-k]*d[k+1]≡[k+1]*d[k] : [n-k]*d[k+1] ≡ [k+1]*d[k]
-    [n-k]*d[k+1]≡[k+1]*d[k] = begin-equality
-      [n-k]*d[k+1]
-        ≡⟨ x∙yz≈y∙xz [n-k] [k+1]! [n-k-1]! ⟩
-      [k+1]! * ([n-k] * [n-k-1]!)
-        ≡⟨ *-assoc (suc k) k! ([n-k] * [n-k-1]!) ⟩
-      (suc k) * (k! * ([n-k] * [n-k-1]!))
-        ≡⟨ cong ((suc k) *_) (cong (k! *_) [n-k]*[n-k-1]!≡[n-k]!) ⟩
-      [k+1]*d[k]             ∎
-      where open CommSemigroupProperties *-commutativeSemigroup
-
     instance
       [k+1]!*[n-k]!≢0 = (suc k) !* [n-k] !≢0
       d[k]≢0          = k !* [n-k] !≢0
       d[k+1]≢0        = (suc k) !* (n ∸ suc k) !≢0
       [k+1]*d[k]≢0    = m*n≢0 (suc k) d[k]
       [n-k]≢0         = ≢-nonZero (m>n⇒m∸n≢0 k<n)
-      [n-k]*d[k]≢0    = m*n≢0 [n-k] d[k]
       [n-k]*d[k+1]≢0  = m*n≢0 [n-k] d[k+1]

src/Data/Nat/Combinatorics/Specification.agda

@@ -98,7 +98,6 @@ k!∣nP′k n@{suc n-1} k@{suc k-1} k≤n@(s≤s k-1≤n-1) with k-1 ≟ n-1
   (subst (k ! ∣_) (nP′k≡n!/[n∸k]! k≤n) (k!∣nP′k k≤n))
   where instance _ = (n ∸ k) !≢0
 
-
 ------------------------------------------------------------------------
 -- Properties of _P_
 

src/Data/Nat/Properties.agda

@@ -121,10 +121,6 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n))
 <ᵇ-reflects-< : ∀ m n → Reflects (m < n) (m <ᵇ n)
 <ᵇ-reflects-< m n = fromEquivalence (<ᵇ⇒< m n) <⇒<ᵇ
 
-n<ᵇ1+n : ∀ n → (n <ᵇ suc n) ≡ true
-n<ᵇ1+n zero = refl
-n<ᵇ1+n (suc n) = n<ᵇ1+n n
-
 ------------------------------------------------------------------------
 -- Properties of _≤ᵇ_
 ------------------------------------------------------------------------
@@ -1577,9 +1573,6 @@ m≤n⇒n∸m≤n (s≤s m≤n) = m≤n⇒m≤1+n (m≤n⇒n∸m≤n m≤n)
   (m + n) ∸ o          ≡⟨ +-∸-assoc m o≤n ⟩
   m + (n ∸ o)          ∎
 
-[m-n-1]+1≡[m-n] : ∀ {m n} (n<m : n < m) → suc (m ∸ suc n) ≡ m ∸ n
-[m-n-1]+1≡[m-n] n<m = sym (+-∸-assoc 1 n<m)
-
 m≤n+m∸n : ∀ m n → m ≤ n + (m ∸ n)
 m≤n+m∸n zero    n       = z≤n
 m≤n+m∸n (suc m) zero    = ≤-refl
@@ -1940,7 +1933,7 @@ n≡⌈n+n/2⌉ (suc n′@(suc n)) =
   cong suc (trans (n≡⌈n+n/2⌉ _) (cong ⌈_/2⌉ (sym (+-suc n n′))))
 
 ------------------------------------------------------------------------
--- Properties of _!
+-- Properties of !_
 
 1≤n! : ∀ n → 1 ≤ n !
 1≤n! zero    = ≤-refl