A proof of the divergence of the harmonic series with the Coq proof assistant.