Library Coq.setoid_ring.RealField
Require
Import
Nnat
.
Require
Import
ArithRing
.
Require
Export
Ring
Field
.
Require
Import
Rdefinitions
.
Require
Import
Rpow_def
.
Require
Import
Raxioms
.
Open
Local
Scope
R_scope
.
Lemma
RTheory
:
ring_theory
0 1
Rplus
Rmult
Rminus
Ropp
(
eq
(
A
:=
R
)).
Lemma
Rfield
:
field_theory
0 1
Rplus
Rmult
Rminus
Ropp
Rdiv
Rinv
(
eq
(
A
:=
R
)).
Lemma
Rlt_n_Sn
:
forall
x
,
x
<
x
+
1.
Notation
Rset
:= (
Eqsth
R
).
Notation
Rext
:= (
Eq_ext
Rplus
Rmult
Ropp
).
Lemma
Rlt_0_2
: 0
<
2.
Lemma
Rgen_phiPOS
:
forall
x
,
InitialRing.gen_phiPOS1
1
Rplus
Rmult
x
>
0.
Lemma
Rgen_phiPOS_not_0
:
forall
x
,
InitialRing.gen_phiPOS1
1
Rplus
Rmult
x
<>
0.
Lemma
Zeq_bool_complete
:
forall
x
y
,
InitialRing.gen_phiZ
0%
R
1%
R
Rplus
Rmult
Ropp
x
=
InitialRing.gen_phiZ
0%
R
1%
R
Rplus
Rmult
Ropp
y
->
Zeq_bool
x
y
=
true
.
Lemma
Rdef_pow_add
:
forall
(
x
:
R
) (
n
m
:
nat
),
pow
x
(
n
+
m
)
=
pow
x
n
*
pow
x
m
.
Lemma
R_power_theory
:
power_theory
1%
R
Rmult
(
eq
(
A
:=
R
))
nat_of_N
pow
.
Ltac
Rpow_tac
t
:=
match
isnatcst
t
with
|
false
=>
constr
:(
InitialRing.NotConstant
)
|
_
=>
constr
:(
N_of_nat
t
)
end
.
Add
Field
RField
:
Rfield
(
completeness
Zeq_bool_complete
,
power_tac
R_power_theory
[
Rpow_tac
]).