Complete Coq formalization of Gödel's ontological proof of God's existence

God exists in Coq too!