∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (a b c : ℤ)
  (h : a + b = c),
  CategoryTheory.shiftFunctorAdd' (CategoryTheory.Pretriangulated.Triangle C) a b c h =
    CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' C a b c h