It’s probably just because a zstd implementation in Lean would be more difficult. The whole project depends on being able to have a correctness proof for the implementation, and implementing that for the DEFLATE algorithm is simpler.