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

[Dr. ERDI Gergo]

Nils,

Would it make sense to add Irreducible to the standard library? Here's the 
generalization I have in mind:

open import Algebra
open import Relation.Nullary
open import Data.Sum
open import Level using (Level; _⊔_)
import Algebra.FunctionProperties

module _ {c ℓ : Level} (R : Algebra.CommutativeSemiring c ℓ) where

open CommutativeSemiring R

private
   infix 4 _≉_

   _≉_ : Carrier → Carrier → Set ℓ
   x ≉ y = ¬ (x ≈ y)

   open Algebra.FunctionProperties _≈_

   is0 : Carrier → Set _
   is0 n = Identity n _+_

   is1 : Carrier → Set _
   is1 n = Identity n _*_

data Irreducible (n : Carrier) : Set (ℓ ⊔ c) where
   irreducible : (not0 : ¬ is0 n) → (not1 : ¬ is1 n) →
                 (prf : ∀ x y → ≈ x * y → is1 x ⊎ is1 y) →
                 Irreducible n

I've also reworked my proof that Irreducible => Prime for Data.Nat to use 
the above generalization and it's definitely not too bad. I haven't ported 
the other direction yet, but will do if we decide it's worth adding to the 
stdlib.

Bye,
 	Gergo