∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Preadditive C] {R : Type u_3}
  [inst_2 : Ring R] [inst_3 : CategoryTheory.Linear R C] {F G : CochainComplex C ℤ} {n : ℤ} (x x_1 : R)
  (x_2 : CochainComplex.HomComplex.Cocycle F G n), (x * x_1) • x_2 = x • x_1 • x_2