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

[IKEGAMI Daisuke]

Thanks for comments!

2011/11/7 Arseniy Alekseyev <arseniy.alekseyev at gmail.com>:
> I know of three ways of representing positive numbers:
> (snip)

The idea did not occur to me. I totally agree that approaches 2 and 3,
which you wrote, are better than the naive approach 1. I will compare
them for the proof that natural numbers without zero forms a
cancellative commutative monoid. I'm pleased to quote Arseniy's idea
to my slides of talk. Thanks.

2011/11/8 Andreas Abel <andreas.abel at ifi.lmu.de>:
> A ring element p is prime if
>
>  p | a*b  implies  p | a or p | b

FYI, in Thierry's proof, he choose the above definition, which you wrote.
I'm not sure whether to prove 2 is prime with the above definition can be
found by the proof, which Nils shows in the previous email.

Best wishes,
Ike