∀ {J : Type u_1} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) (n : ℕ)
  (a : RingCat.Colimits.ColimitType F),
  zsmulRec nsmulRec (Int.negSucc n) a = Quotient.map RingCat.Colimits.Prequotient.neg ⋯ (zsmulRec nsmulRec (↑n.succ) a)