∀ {J : Type u_1} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) (n : ℕ)
  (a : RingCat.Colimits.ColimitType F), SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a