(*#* The term [Z_as_CSetoid] is of type [CSetoid]. Hence we have proven that [Z] is a constructive setoid.
***Addition
We will prove now that the addition on the integers is a setoid function.
*)
(*#* The term [Z_as_CSetoid] is of type [CSetoid]. Hence we have proven that [Z] is a constructive setoid.
***Addition
We will prove now that the addition on the integers is a setoid function.
*)