∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] [inst_1 : LinearOrder ι] (s : Finset ι) (f g : ι → R),
  ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j