∀ {G : Type u_1} {G' : Type u_2} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedAddMonoid G]
  [inst_3 : AddCommGroup G'] [inst_4 : LinearOrder G'] [inst_5 : IsOrderedAddMonoid G'] (x : G) (y : G')
  (xpos : 0 < max x (-x)) (ypos : 0 < max y (-y)) (hxc : AddSubgroup.closure {x} = AddSubgroup.closure {max x (-x)})
  (hyc : AddSubgroup.closure {y} = AddSubgroup.closure {max y (-y)}) (a b : ↥(AddSubgroup.closure {x})),
  { toFun := fun a => ⟨⋯.choose • max y (-y), ⋯⟩, invFun := fun a => ⟨⋯.choose • max x (-x), ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }.toFun
      (a + b) =
    { toFun := fun a => ⟨⋯.choose • max y (-y), ⋯⟩, invFun := fun a => ⟨⋯.choose • max x (-x), ⋯⟩, left_inv := ⋯,
            right_inv := ⋯ }.toFun
        a +
      { toFun := fun a => ⟨⋯.choose • max y (-y), ⋯⟩, invFun := fun a => ⟨⋯.choose • max x (-x), ⋯⟩, left_inv := ⋯,
            right_inv := ⋯ }.toFun
        b