rw [Ici_eq_cons_Ioi, prod_cons]
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : CommMonoid β
f : α → β
a✝ b : α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ f a * ∏ x ∈ Ioi a, f x = ∏ x ∈ Ici a, f x
no goals