moved lemma

Author: jamesmckinna

CHANGELOG.md

@@ -2121,16 +2121,12 @@ Other minor changes
 
 * Added new proofs in `Data.Nat.Combinatorics`:
   ```agda
+  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
   ```
 
-* Added new proofs in `Data.Nat.Combinatorics.Specification`:
-  ```agda
-  k![n∸k]!∣n! : k ≤ n →  k ! * (n ∸ k) ! ∣ n !
-  ```
-
 * Added new proofs in `Data.Nat.DivMod`:
   ```agda
   m%n≤n           : .{{_ : NonZero n}} → m % n ≤ n

src/Data/Nat/Combinatorics.agda

@@ -36,7 +36,7 @@ open Base public
 -- Properties of _P_
 
 open Specification public
-  using (nPk≡n!/[n∸k]!; k>n⇒nPk≡0; [n∸k]!k!∣n!; k![n∸k]!∣n!)
+  using (nPk≡n!/[n∸k]!; k>n⇒nPk≡0; [n∸k]!k!∣n!)
 
 nPn≡n! : ∀ n → n P n ≡ n !
 nPn≡n! n = begin-equality
@@ -109,6 +109,9 @@ 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 !
+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
 nCk+nC[k+1]≡[n+1]C[k+1] n k with <-cmp k n
 {- case k>n, in which case 1+k>1+n>n -}

src/Data/Nat/Combinatorics/Specification.agda

@@ -98,9 +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
 
-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)
-
 
 ------------------------------------------------------------------------
 -- Properties of _P_