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? How about something simple & straightforward like this: https://gist.github.com/gergoerdi/a70e414484a5d0ab97e0