Library Coq.Reals.LegacyRfield
Require
Export
Raxioms
.
Require
Export
LegacyField
.
Import
LegacyRing_theory
.
Section
LegacyRfield
.
Open
Scope
R_scope
.
Lemma
RLegacyTheory
:
Ring_Theory
Rplus
Rmult
1 0
Ropp
(
fun
x
y
:
R
=>
false
).
End
LegacyRfield
.
Add
Legacy
Field
R
Rplus
Rmult
1%
R
0%
R
Ropp
(
fun
x
y
:
R
=>
false
)
Rinv
RLegacyTheory
Rinv_l
with
minus
:=
Rminus
div
:=
Rdiv
.