no goals
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝ : α
g f✝ : α → β
inst✝ : CommMonoid β
a b : ℕ
hab : a ≤ b
f : ℕ → β
⊢ ∏ k in Ioc a (b + 1), f k = (∏ k in Ioc a b, f k) * f (b + 1)
rw [← prod_Ioc_consecutive _ hab (Nat.le_succ b), Nat.Ioc_succ_singleton, prod_singleton]