Harrison, J. “A Formalized Proof of Dirichlet’s Theorem on Primes in Arithmetic Progression”. Journal of Formalized Reasoning, vol. 2, no. 1, Jan. 2009, pp. 63-83, doi:10.6092/issn.1972-5787/1558.