[Agda] Re: Data.Nat.Primality.Prime and irreducibility

[N. Raghavendra]

At 2015-03-06T13:46:21+04:00, Sergei Meshveliani wrote:

> Personally, I use a generic primality definition for any GCDRing 
> (an integral ring with GCD):
>
>   IsPrime : C → Set (α ⊔ α=)
>   IsPrime a =  a ≉ 0#  ×  ¬ Invertible a  ×
>                (∀ {x y} → (x * y ≈ a) → Invertible x ⊎ Invertible y),
>
> which, I think, is the classical definition.
> Then, I prove several lemmata about possible Factorization structure for
> the elements of such a ring, and find that this my definition works all
> right.

Thanks!  However, my question was specially about how to prove that the
Data.Nat.Primality definition of an element n of N being Prime is
equivalent to n being irreducible in the multiplicative monoid of
non-zero natural numbers.

Have you put your proofs on the Web?

Cheers,
Raghu.

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