github.com/coq/opam-coq-archive
Coq proof of the correctness of the Huffman coding algorithm
opam install coq-huffman.8.12.0