Library Stdlib.setoid_ring.Rings_Z

From Stdlib Require Export Cring.
From Stdlib Require Export Integral_domain.
From Stdlib 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.