Isolate the numerics of an analytic-combinatorics proof as a ∀-hypothesis

In a Lean proof chaining a Fourier bound, a geometric lemma and a combinatorial theorem (e.g. Freiman 2.4 in ZMod p), state the core theorem with the single real inequality the argument consumes as a hypothesis, e.g. hnum : ∀ (n : ℕ) (Q : ℝ), 0 ≤ Q → k^3*(p-T) ≤ Q*(p-k)*T → √Q*γ ≤ 2*n-k → T+3 < 3*n. Each constant variant (2.4 with p ≥ 12k, 2.45 with p ≥ 100k) is then a 20-line corollary plus one nlinarith lemma. For those lemmas, by_contra and step down through explicit rational constants (Q ≤ (180/499)k², then k(p-T) ≤ c(p-k)T). End with nlinarith [mul_nonneg (p - 12k ≥ 0) (k - cT ≥ 0)]. One nlinarith call on the raw hypotheses times out. Gotcha: in the core proof omega does not know p > 0 from Fact p.Prime, so add have := hp.out.two_le first. Otherwise omega gives baffling counterexamples with min-terms.