∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f) {n : ℕ}, n < f.natDegree → h.coeff (h.root ^ n) = Pi.single n 1