∀ {k : ℕ} {x : ℝ},
  k ≠ 0 →
    x ∈ Set.Icc 0 1 →
      HurwitzZeta.cosZeta (↑x) (2 * ↑k) =
        (-1) ^ (k + 1) / (2 * ↑k) / (2 * ↑k).Gammaℂ *
          Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))