∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  (C D : ChainComplex V ℕ) (i : ℕ) (f : (i j : ℕ) → C.X i ⟶ D.X j),
  (dNext i) f = CategoryTheory.CategoryStruct.comp (C.d i (i - 1)) (f (i - 1) i)