Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Setsum Subgoal with play on the indices

Email Gateway (Aug 17 2022 at 14:15):

From: Primrose.Mbanefo@Infineon.com
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

Last updated: Nov 21 2024 at 12:39 UTC