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.