split a sum into even and odd terms

Stream: new members

[Kamila Szewczyk]

If I have a sum over Finset.range, how can I split it into even and odd terms of the sum, so that I can prove that either of them vanishes?

[Ruben Van de Velde]

Interesting question. Can you prove range = evens \cup odds?

[Kamila Szewczyk]

Perhaps? the range is just discrete from 0..n