Associated, prime, and irreducible elements. #
In this file we define the predicate Prime p
saying that an element of a commutative monoid with zero is prime.
Namely, Prime p means that p isn't zero, it isn't a unit,
and p ∣ a * b → p ∣ a ∨ p ∣ b for all a, b;
In decomposition monoids (e.g., ℕ, ℤ), this predicate is equivalent to Irreducible,
however this is not true in general.
We also define an equivalence relation Associated
saying that two elements of a monoid differ by a multiplication by a unit.
Then we show that the quotient type Associates is a monoid
and prove basic properties of this quotient.