Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada: A formalization of the Berlekamp-Zassenhaus factorization algorithm. CPP 2017: 17-29