github.com/coq/opam-coq-archive
Verified implementation of Buchberger's algorithm for computing Gröbner bases in Coq
opam install coq-buchberger.8.11.0