[Agda] factorization monoid, ring

[Sergei Meshveliani]

People,

I have fully implemented in Agda 

1) the notion of Factorization Monoid (for a commutative cancellative
monoid)
(as Raghu mentioned last year),

2) the notion of Factorization Ring,
3) the notion factorization uniqueness for such domains,
4) proofs for many lemmata which relate these notions to each other, and
to factorization in a multiplicative monoid of Nat and Integer,

5) factorization by the sieve method for Nat (with a proof). 

It remains to revise a manual (many types and modules have changed) and
to put on the Web the library DoCon-A 0.04 which includes this. 


And I need to compare my approach to what it is done in  Coq 
                                                         ----

with respect to this particular subject -- papers, documentation for
various libraries, not necessarily standard library.

I observe on the Web a couple of libraries in Coq related to 
1) a general algebraic hierarchy (Monoid, Ring, etc),
2) advanced algorithms for factoring integer numbers, and such.

But I do not find:  where there are implemented the general notions of
Factorization Monoid or Factorization Ring,
a notion of factorization uniqueness for such domains, and some generic
lemmata about them?
(papers, documentation -- ?)

Can somebody point at such?

Thanks,

------
Sergei