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

[Nils Anders Danielsson]

On 2011-11-08 03:22, IKEGAMI Daisuke wrote:
> 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.

My definition is definitely non-standard, chosen only to make it easy to
decide whether a number is prime or not. One should probably prove that
this definition is equivalent to a standard one.

-- 
/NAD