Lean-Workbook Plus 60949: Trigonometric inequality

for all real number of $x$ , then $\vert\sin{x}\vert + \vert\cos{x}\vert \geq 1$.

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