Library Coq.setoid_ring.Rings_Z

Require Export Cring.
Require Export Integral_domain.
Require Export Ncring_initial.

#[global]
Instance Zcri: (Cring (Rr:=Zr)).


Lemma Z_one_zero: 1%Z <> 0%Z.

#[global]
Instance Zdi : (Integral_domain (Rcr:=Zcri)).
Defined.