[Agda] Irrationality proof

[N. Raghavendra]

Hi,

I am trying to understand Coquand's formalisation of a proof of the
irrationality of the square root of 2.  (It was discussed here earlier
too, http://thread.gmane.org/gmane.comp.lang.agda/3301/)  He proves that
if A is a cancellative commutative semigroup, and if p is a prime
element of A such that the relation

multiple p = (x -> y -> p*x==y)

on A is Noetherian, then there are no a and b in A such that p*a^2==b^2:

(p:A) -> Prime p -> Noether A (multiple p) -> isNotSquare p.

I am stuck when he says that this applies the case where A is the
semigroup of strictly positive integers, and p is any prime there, e.g.,
2.  I don't see how to prove that the relation (multiple 2) on this A is
Noetherian.  The definition of Noetherian is

(P:Pred A) -> ((x:A) -> ((y:A) -> 2*y==x -> P y) -> P x) -> (x:A) -> P x

Perhaps I am missing something obvious.  Any suggestions?

Thanks and cheers,
Raghu

--
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/