Home
About Coq
Get Coq
Documentation
Community
The Coq Proof Assistant
Library Coq.setoid_ring.Rings_Z
Require
Export
Cring
.
Require
Export
Integral_domain
.
Require
Export
Ncring_initial
.
Require
Export
Omega
.
Instance
Zcri
: (
Cring
(
Rr
:=
Zr
)).
Lemma
Z_one_zero
: 1%
Z
<>
0%
Z
.
Instance
Zdi
: (
Integral_domain
(
Rcr
:=
Zcri
)).
Navigation
Standard Library
Table of contents
Index