∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddMonoid R],
  HahnSeries.addOppositeEquiv =
    { toFun := fun x => AddOpposite.op { coeff := fun a => AddOpposite.unop (x.coeff a), isPWO_support' := ⋯ },
      invFun := fun x => { coeff := fun a => AddOpposite.op ((AddOpposite.unop x).coeff a), isPWO_support' := ⋯ },
      left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }