This is good. I like this a lot.
It's worse than that, it expects True for 7601, 102,5401... False for 20, 1500..
What on Earth
lovely. interesting use of the list difference operator!
Wait, wha- 🤯
Okay: i feel stupid :)
also: i had some problems using them when i did the definition in ltac, for now i just copypasted the output from Show Proof.
i could not use the stream_unfold unless the definition was not in ltac.
Is there any reason odd is a Definition not a CoFixpoint?