∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} (f h : PowerSeries R) {g : Polynomial R},
  g.IsDistinguishedAt I →
    PowerSeries.constantCoeff h ∉ I → f = ↑g * h → ↑g.natDegree = ((PowerSeries.map (Ideal.Quotient.mk I)) f).order