# Setoids for beginners

Although the type **Z** of integers is already defined in Coq, it
is interesting to look at the usual mathematical building of the set of
integers as a quotient of the set of pairs of natural numbers by the
equivalence relation *(a,b) R (c,d)* if *a+d = b+c*.

In Coq, you will associate a setoid to this equivalence relation, and
register the usual operations : **+**, *****, etc, as morphisms.
Prove also that you build a ring with unity and the property of integrity
(*i.e.* if *xy = 0 * then *x = 0 * or
*y = 0 *.)

In a second time, build the ring of integers modulo p (with p:nat).

Give some examples of `setoid_replace` and `setoid_rewrite`.
## Solution