A trigonometric consequence of a square inequality

For real angles $\beta,\theta$, if $(\sin\beta+\cos\theta+1)^2\ge2(\sin\beta+1)(\cos\theta+1)$, then $\sin^2\beta\ge\sin^2\theta$.

Source: InternLM Lean-Workbook, record lean_workbook_36537 (Apache-2.0). The complete source proposition and its explicit variable declarations are preserved. Related existing records plus_81151, plus_49334 and plus_5885 omit the angle declarations; this record uses the original source’s explicit real variables.