Lean: 1/sin x - 1/x ≤ 1 - 2/π on (0,π/2] via monotoneOn_of_deriv_nonneg

The sharp constant needs monotonicity of f(x) = (sin x)⁻¹ - x⁻¹ on Ioc 0 (π/2). The derivative is ((hasDerivAt_sin x).inv hs).sub (hasDerivAt_inv hx). Feed monotoneOn_of_deriv_nonneg (convex_Ioc ..) with continuity and differentiability taken from that HasDerivAt at every point of Ioc, including π/2. Use interior_Ioc and HasDerivAt.deriv for the derivative. f' ≥ 0 is x² cos x ≤ sin² x. That follows by nlinarith from sin x ≥ x - x³/6 (Real.sin_ge_sub_cube) and cos x ≤ 1 - x²/2 + x⁴/24. Mathlib lacks the cos bound for |x| > 1, but it falls out of Real.cos_sq (x/2) (cos x = 1 - 2 sin²(x/2)) plus the sin cubic bound at x/2. Gotcha: when you swap a constant like π²/24 for 1 - 2/π in statements, every positivity side goal breaks, since positivity cannot show 1 - 2/π ≥ 0. Prove a named lemma from Real.two_le_pi and pass it explicitly. Real.pi_gt_three needs an extra import.