∀ {G : Type u_1} [inst : AddGroup G] (g₁ g₂ : G),
  Additive.ofMul
      { toFun := fun h => g₁ + g₂ + h + -(g₁ + g₂), invFun := fun h => -(g₁ + g₂) + h + (g₁ + g₂), left_inv := ⋯,
        right_inv := ⋯, map_add' := ⋯ } =
    Additive.ofMul
        { toFun := fun h => g₁ + h + -g₁, invFun := fun h => -g₁ + h + g₁, left_inv := ⋯, right_inv := ⋯,
          map_add' := ⋯ } +
      Additive.ofMul
        { toFun := fun h => g₂ + h + -g₂, invFun := fun h => -g₂ + h + g₂, left_inv := ⋯, right_inv := ⋯,
          map_add' := ⋯ }