Complementary choices in a shifted set size

For natural numbers $n,k$,

Here $n-1$ uses natural subtraction, so it is zero when $n=0$.

This restores the missing imports or namespaces of the original node, retaining its formal proposition. Source: Lean-Workbook row lean_workbook_plus_10295 (Apache-2.0).