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

[Dr. ERDI Gergo]

On Fri, 6 Mar 2015, N. Raghavendra wrote:

> That's nice!  Many thanks.  I'll learn from it.
>
> Can you also send me a proof of Prime -> Irreducible?  As I said, I've
> an unwieldy proof of that implication, and would like to know how to
> improve upon it.  In my proof I don't use Prime directly, but use
> prime->coprime from Data.Nat.Coprimality.

I've updated the same gist at https://gist.github.com/gergoerdi/a70e414484a5d0ab97e0
but because I'm not good with arithmetic proofs, it's pretty unwieldy 
itself. But at least it doesn't go throgh Coprimality. Let me know what 
you think about it.