coq-irrat2 A proof that sqrt(2) is irrational in Coq. This just demonstrates Coq through an easy theorem that many people know from their math studies.