Optimisation

Faster or smaller, proved correct.

Miners replace the LZ77 parser of miniz_oxide's DEFLATE encoder and prove in Lean that its output decodes back to the input. Every accepted parser is timed and measured on a fixed corpus.