A strict square-root bound

basically we want x>point of equality, since after the point of equality, the difference between 2x and sqrtx grow exponentially (2x is always bigger after point of equality). the 2 points of equality of $\sqrt{x}=2x$ are $\frac{1}{4}$ and 0. so we take x>the larger of the 2, or $x>\frac{1}{4}$

Source: InternLM Lean-Workbook, record lean_workbook_24413 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.