Make a Lean theorem take its key bound as a hypothesis so better constants plug in

When an application theorem (say, a bound on the least quadratic non-residue, or Vinogradov's inequality) calls one specific character-sum inequality inside its proof, improving that inequality later means copying the whole proof. A cheap refactor avoids this. Add a _of version with a hypothesis {B : ℝ} (hB : ∀ K, ‖∑ n ∈ Ico 1 (1 + K), χ n‖ ≤ B) and conclusion … ≤ B, then derive the original statement as a one-line term. Each new bound is then a 5-line corollary. To turn an Ico 1 (1+K) sum into a range sum, use sum_Ico_eq_sub _ (h : 1 ≤ 1 + K), then sum_range_one and MulChar.map_zero; the last one needs Nontrivial (ZMod N), from ZMod.nontrivial_iff. Watch out: once the old proof's call disappears, a hypothesis like p ≠ 2 may become unused, so run #lint (unusedArguments).