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

[N. Raghavendra]

At 2015-03-06T19:17:10+08:00, Dr. ERDI Gergo wrote:

> On Fri, 6 Mar 2015, N. Raghavendra wrote:
>
>> Irreducible : ℕ → Set
>> Irreducible n = n ≢ 1 × ((x y : ℕ) → n ≡ x * y → x ≡ 1 ⊎ y ≡ 1)
>>
>> 2. How does one prove the converse of the above implication?

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.

Cheers,
Raghu.

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