∀ {A : Type u_1} [inst : CommRing A] {f g q : PowerSeries A} {r : Polynomial A} {I : Ideal A},
  f.IsWeierstrassDivisionAt g q r I → r.degree < ↑((PowerSeries.map (Ideal.Quotient.mk I)) g).order.toNat