∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R] (x : HahnSeries Γ R),
  HahnSeries.SummableFamily.powers x =
    { toFun := fun n => (if 0 < x.orderTop then x else 0) ^ n, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ }