[isabelle] Setsum Subgoal with play on the indices



Hi,

I have a subgoal which basically looks like:
\<Sum>i=0..<X. f (Suc i) = \<Sum>i=1..X. f i

And one of the assumptions is that 0 < X.

I have tried looking it up and came upon setsum_reindex which seems to
fit but I do not know how to use it in this case.
How can I go about proving this?

Thanks in advance for any help.

Primrose





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.