∀ {M : Type u_2} [inst : AddMonoid M],
  AddUnits.opEquiv =
    {
      toFun := fun u =>
        AddOpposite.op { val := AddOpposite.unop ↑u, neg := AddOpposite.unop ↑(-u), val_neg := ⋯, neg_val := ⋯ },
      invFun := fun X =>
        AddOpposite.rec'
          (fun u => { val := AddOpposite.op ↑u, neg := AddOpposite.op ↑(-u), val_neg := ⋯, neg_val := ⋯ }) X,
      left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }