[Agda] A proof of the irrationality of the square root in Agda

[IKEGAMI Daisuke]

Hi everyone,

To be familiar with Agda, I translated a proof in Agda1/Alfa to the
current Agda as an exercise.

The proof was written by Thierry Coquand; which shows any prime
cannot be a square of rational in any cancellative abelian monoid [1]
for the paper "The seventeen provers of the world" [2, 3];
ed. Freek Wiedijk.

I'm satisfied that everything in the file is translated, well-typed
and terminated [4]. The proof of the principle of infinite descent,
following Fermat, becomes shorter than original one in
Agda1/Alfa thanks to the features of Agda, s.t. the with-notation.
In my opinion, some proofs in Agda can be more readable than
Agda1/Alfa. I learned few tips for translation manually.
Of course, automatic translator shall be better, however, it seems
not easy, I think.

Though translating has been finished, I still work for another
proofs to show the square root of 2 is irrational, which the paper was
requested. Because Thierry shows the abstract theorem in a
cancellative abelian monoid, but, there is no proof about the set of
natural numbers, we need to prove several propositions as following:

DONE
- the natural numbers without zero with multiplication forms a
  an abelian monoid [NEW!, easy thanks to the Agda library]
TODO (still working)
- the natural numbers without zero with multiplication is cancellative
- 2 is prime
- "multiple 2" is Noetherian (see also the definition in files)

[1] http://www.cs.ru.nl/~freek/comparison/files/agda.alfa
[2] http://www.cs.ru.nl/~freek/comparison/
[3] http://www.cs.ru.nl/~freek/comparison/comparison.pdf
[4] https://github.com/IKEGAMIDaisuke/Pythagoras

I struggle to prove the above propositions. I don't know whether we
can prove them or not, I mean, not sure dependent type-theoretical
difficulties. Comments or pull requests are always welcome.

Best wishes,
Ike