{G : Type u} →
  {P : Sort u_1} →
    {toAddMonoid : AddMonoid G} →
      {toNeg : Neg G} →
        {toSub : Sub G} →
          {sub_eq_add_neg : autoParam (∀ (a b : G), a - b = a + -b) SubNegMonoid.sub_eq_add_neg._autoParam} →
            {zsmul : ℤ → G → G} →
              {zsmul_zero' : autoParam (∀ (a : G), zsmul 0 a = 0) SubNegMonoid.zsmul_zero'._autoParam} →
                {zsmul_succ' :
                    autoParam (∀ (n : ℕ) (a : G), zsmul (↑n.succ) a = zsmul (↑n) a + a)
                      SubNegMonoid.zsmul_succ'._autoParam} →
                  {zsmul_neg' :
                      autoParam (∀ (n : ℕ) (a : G), zsmul (Int.negSucc n) a = -zsmul (↑n.succ) a)
                        SubNegMonoid.zsmul_neg'._autoParam} →
                    {toAddMonoid' : AddMonoid G} →
                      {toNeg' : Neg G} →
                        {toSub' : Sub G} →
                          {sub_eq_add_neg' :
                              autoParam (∀ (a b : G), a - b = a + -b) SubNegMonoid.sub_eq_add_neg._autoParam} →
                            {zsmul' : ℤ → G → G} →
                              {zsmul_zero'' :
                                  autoParam (∀ (a : G), zsmul' 0 a = 0) SubNegMonoid.zsmul_zero'._autoParam} →
                                {zsmul_succ'' :
                                    autoParam (∀ (n : ℕ) (a : G), zsmul' (↑n.succ) a = zsmul' (↑n) a + a)
                                      SubNegMonoid.zsmul_succ'._autoParam} →
                                  {zsmul_neg'' :
                                      autoParam (∀ (n : ℕ) (a : G), zsmul' (Int.negSucc n) a = -zsmul' (↑n.succ) a)
                                        SubNegMonoid.zsmul_neg'._autoParam} →
                                    { toAddMonoid := toAddMonoid, toNeg := toNeg, toSub := toSub,
                                          sub_eq_add_neg := sub_eq_add_neg, zsmul := zsmul, zsmul_zero' := zsmul_zero',
                                          zsmul_succ' := zsmul_succ', zsmul_neg' := zsmul_neg' } =
                                        { toAddMonoid := toAddMonoid', toNeg := toNeg', toSub := toSub',
                                          sub_eq_add_neg := sub_eq_add_neg', zsmul := zsmul',
                                          zsmul_zero' := zsmul_zero'', zsmul_succ' := zsmul_succ'',
                                          zsmul_neg' := zsmul_neg'' } →
                                      (toAddMonoid ≍ toAddMonoid' →
                                          toNeg ≍ toNeg' → toSub ≍ toSub' → zsmul ≍ zsmul' → P) →
                                        P