∀ {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) ⦃x y : S⦄, (∀ i < f.natDegree, h.coeff x i = h.coeff y i) → x = y