∀ {G : Type u_1} {G' : Type u_2} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G]
  [inst_3 : AddCommGroup G'] [inst_4 : LinearOrder G'] [IsOrderedAddMonoid G'] (x : G) (y : G'),
  0 < max x (-x) →
    0 < max y (-y) →
      ∀ (hxc : AddSubgroup.closure {x} = AddSubgroup.closure {max x (-x)})
        (hyc : AddSubgroup.closure {y} = AddSubgroup.closure {max y (-y)}),
        Function.RightInverse (fun a => ⟨⋯.choose • max x (-x), ⋯⟩) fun a => ⟨⋯.choose • max y (-y), ⋯⟩