## Harmonic Divergence in Coq

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