The integer part of pi

The greatest integer less than $\pi$ is $3$ , so $\lfloor \pi\rfloor = 3$ .

Source: InternLM Lean-Workbook, record lean_workbook_plus_47995 (Apache-2.0). Complete source proposition preserved; proof developed independently.