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

[N. Raghavendra]

At 2015-03-06T23:39:35+08:00, Dr. ERDI Gergo wrote:

> 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.

Thanks for that too!  It is shorter than the proof I had, and it uses
the SemiringSolver which I didn't know about.  So it's useful to see
your proof.

Cheers,
Raghu.

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