∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : PartialOrder Γ']
  (x : HahnSeries Γ (HahnSeries Γ' R)), x.ofIterate = { coeff := fun g => (x.coeff g.1).coeff g.2, isPWO_support' := ⋯ }