The pure Lean implementation of zstd in that project is only decompression, not compression. It kind of proves my point.