∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] (x : G),
  AddSubgroup.closure {x} = AddSubgroup.closure {max x (-x)} →
    ∀ (a : ↥(AddSubgroup.closure {x})), ∃ n, n • max x (-x) = ↑a