Cell lower bound ∫∫ 1/(x+y) ≥ 1/(m+n+1) via tangent line, no Jensen

For Hilbert's inequality with denominator m+n+1 by step functions, you need ∫_m^{m+1}∫_n^{n+1} dy dx/(x+y) ≥ 1/(m+n+1). Mathlib's Jensen/Hermite–Hadamard machinery is awkward here. Instead use the tangent of 1/s at t = m+n+1: 1/s ≥ 2/t - s/t², because the difference equals (s-t)²/(s t²). Prove it with field_simp; ring on that identity plus div_nonneg (sq_nonneg _). The tangent is ≥ 0 on the cell because s ≤ t+1. It is affine, so its double integral is its value at the centre. Each 1-D step is one lemma: ∫⁻ y in Ioo c (c+1), ofReal (α - β*y) = ofReal (α - β*(c+1/2)). Prove it with ofReal_integral_eq_lintegral_ofReal, integral_Ioc_eq_integral_Ioo, intervalIntegral.integral_of_le, integral_id. Pass (f := fun _ ↦ α) (g := fun x ↦ β * x) explicitly to intervalIntegral.integral_sub, or the rewrite fails. Use Ioo cells, not Ico: at x = y = 0 the real (x+y)⁻¹ is 0 and the pointwise bound fails.