Unable to use to_additive in prod_Ico_succ_top

Stream: mathlib4

[Yongxi Lin (Aaron)]

Right now Finset.prod_Ico_succ_top is only proved for ℕ-indexed sequences. I would like to generalize this to any α such that it satisfies

[LinearOrder α] [LocallyFiniteOrder α] [One α] [Add α] [SuccAddOrder α].

In fact, the same proof works:

import Mathlib

open Finset

variable {α M : Type*} [CommMonoid M]

theorem prod_Ico_succ_top' [LinearOrder α] [LocallyFiniteOrder α] [One α] [Add α] [SuccAddOrder α]
    [NoMaxOrder α] {a b : α} (hab : a ≤ b) (f : α → M) :
    (∏ k ∈ Ico a (b + 1), f k) = (∏ k ∈ Ico a b, f k) * f b := by
  rw [← Finset.insert_Ico_right_eq_Ico_add_one hab, prod_insert right_notMem_Ico, mul_comm]

But to_additive does not work after I did this generalization. I believe this is because to_additive turns [One α] into [Zero α], but [SuccAddOrder α] need the former instead of the latter. I am not very familiar with to_additive, so I am not sure what is the correct way of fixing this problem.

[Floris van Doorn]

Please try @[to_additive (dont_translate := α)]

[Yongxi Lin (Aaron)]

It is working! Thank you for your help. :smile: