∀ {n : ℕ} {B₁ B₂ : Fin (n + 1) → ℝ}
  (p : ↑{p | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), B₁ i ≤ ↑(p.coeff ↑i) ∧ ↑(p.coeff ↑i) ≤ B₂ i}),
  ((Polynomial.ofFn (n + 1)) ↑⟨(Polynomial.toFn (n + 1)) ↑p, ⋯⟩).natDegree ≤ n ∧
    ∀ (i : Fin (n + 1)),
      B₁ i ≤ IntCast.intCast (((Polynomial.ofFn (n + 1)) ↑⟨(Polynomial.toFn (n + 1)) ↑p, ⋯⟩).coeff ↑i) ∧
        IntCast.intCast (((Polynomial.ofFn (n + 1)) ↑⟨(Polynomial.toFn (n + 1)) ↑p, ⋯⟩).coeff ↑i) ≤ B₂ i