LeanSieve 5: live-proving: Rake

Down to the last data structure in my Prime Sieve. This one's a bit different, because I have to prove properties of Lists rather than just numbers.