Author:
Ikegami Daisuke <ikegami.da@gmail.com>

An example : Translate Agda1/Alfa to Agda2
Sqrt 2 is not rational. Works with the Agda standard library.

Links:
Agda
  http://wiki.portal.chalmers.se/agda/pmwiki.php
Agda standard library
  http://wiki.portal.chalmers.se/agda/agda.php?n=Libraries.StandardLibrary
the original proof on Agda1/Alfa
  http://www.cs.ru.nl/~freek/comparison/files/agda.alfa
the paper
  http://www.cs.ru.nl/~freek/comparison/comparison.pdf
Other proofs by another different proof assistants
  http://www.cs.ru.nl/~freek/comparison/

Files:
Cancel.agda 
  the definition of cancel
CancellativeAbelianMonoid.agda
  the definition of cancellative abelian monoid
Corollary.agda
  the set of the natural numbers without zero and multiplication
  forms a cancellative abelian modoid. Thus, square root of two
  is irrational
Lemma.agda
  lemmata for the proof of the main theorem in Theorem.agda
NatStar.agda
  A set of natural numbers without zero, and its multiplication
NatStarProperties.agda
  Properties of NatStar
Noether.agda
  the definitions of Noetherian and Fermat's infinite descent
  principle
Property.agda
  helper functions of a cancellative abelian monoid
Theorem.agda
  the main theorem which is originally proved by Thierry Coquand;
  any prime cannot be a square of rational in cancellative abelian
  monoid

Note:
agda.alfa was written by Thierry Coquand.