Library Coq.setoid_ring.Rings_R
Require
Export
Cring
.
Require
Export
Integral_domain
.
Require
Import
Reals
.
Require
Import
RealField
.
Lemma
Rsth
:
Setoid_Theory
R
(@
eq
R
).
Instance
Rops
: (@
Ring_ops
R
0%
R
1%
R
Rplus
Rmult
Rminus
Ropp
(@
eq
R
)).
Defined
.
Instance
Rri
: (
Ring
(
Ro
:=
Rops
)).
Defined
.
Instance
Rcri
: (
Cring
(
Rr
:=
Rri
)).
Lemma
R_one_zero
: 1%
R
<>
0%
R
.
Instance
Rdi
: (
Integral_domain
(
Rcr
:=
Rcri
)).