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

[N. Raghavendra]

Hi,

I am looking at the type

Irreducible : ℕ → Set
Irreducible n = n ≢ 1 × ((x y : ℕ) → n ≡ x * y → x ≡ 1 ⊎ y ≡ 1)

I am able to prove

primen⇒irreduciblen : (n : ℕ) →
  Data.Nat.Primality.Prime n → Irreducible n

I've some questions:

1. Is there a short proof of this implication?  The one I wrote is a bit
long.

2. How does one prove the converse of the above implication?

3. Is there some special reason for defining Prime as in
Data.Nat.Primality, instead of something like

Prime : ℕ → Set
Prime n = n ≢ 1 × ((x y : ℕ) → n | x * y → n | x ⊎ n | y)

as is common in informal mathematics?

Thanks and cheers,
Raghu.

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