6.2 Stirling numbers of the first kind
\(c(n, k) = \# \{ \sigma \in \mathfrak {S}_{n} : c(\sigma ) = k\} \) counts permutations of \(\{ 0, \dots , n-1\} \) with exactly \(k\) cycles in their disjoint-cycle decomposition. Stanley writes \(c(n, k)\) throughout §1.3.2.
\(\sum _{k=0}^{n} c(n, k) = n!\). Each permutation is counted by exactly one \(k\), so the row sum recovers the total.
For all \(n, k \in \mathbb {N}\),
Combinatorially: \(n+1\) either becomes a fixed point of a \(k\)-cycle permutation (giving \(c(n, k)\)), or is inserted into one of \(n\) positions of a \((k+1)\)-cycle permutation (giving \(n \cdot c(n, k+1)\)).
Formalization route. The proof factors through a construction \(\mathrm{insert\_ after}\, j_0\, s : \mathfrak {S}_{n+1}\) that splices \(\mathrm{ord\_ max}\) into the \(s\)-cycle through \(j_0\). The key algebraic identity
reduces cycle-count preservation to MathComp’s porbits_mul_tperm composed with the fixed-point cycle-count lemma in .