∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ) (n i : ℤ),
  autoParam (i < n) CochainComplex.isZero_of_isStrictlyGE._auto_1 →
    ∀ [K.IsStrictlyGE n], CategoryTheory.Limits.IsZero (K.X i)