LeanSieve 6: even more live-proving

This ought to be close to the final stretch, but who can say? I continue to work to verify my simple prime sieve implementation in lean 4.