Library Coq.setoid_ring.Rings_Q
Require
Export
Cring
.
Require
Export
Integral_domain
.
Require
Import
QArith
.
Instance
Qops
: (@
Ring_ops
Q
0%
Q
1%
Q
Qplus
Qmult
Qminus
Qopp
Qeq
).
Defined
.
Instance
Qri
: (
Ring
(
Ro
:=
Qops
)).
Defined
.
Instance
Qcri
: (
Cring
(
Rr
:=
Qri
)).
Lemma
Q_one_zero
:
not
(
Qeq
1%
Q
0%
Q
).
Instance
Qdi
: (
Integral_domain
(
Rcr
:=
Qcri
)).