Lean-Workbook Plus 38834: Trigonometric inequality

Lean-Workbook Plus 38834: Middle binomial coefficient bound

For natural numbers $n,k$ with $k\le n$, $\binom nk\le\binom n{\lfloor n/2\rfloor}$.

Source: Lean-Workbook row lean_workbook_plus_38834 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.