Library Coq.nsatz.Nsatz
Require
Import
List
.
Require
Import
Setoid
.
Require
Import
BinPos
.
Require
Import
BinList
.
Require
Import
Znumtheory
.
Require
Export
Morphisms
Setoid
Bool
.
Require
Export
Algebra_syntax
.
Require
Export
Ncring
.
Require
Export
Ncring_initial
.
Require
Export
Ncring_tac
.
Require
Export
Integral_domain
.
Require
Import
DiscrR
.
Require
Import
ZArith
.
Require
Import
Lia
.
Require
Export
NsatzTactic
.
Make use of
discrR
in
nsatz
Ltac
nsatz_internal_discrR
::=
discrR
.
Require
Import
Reals
.
Require
Import
RealField
.
Lemma
Rsth
:
Setoid_Theory
R
(@
eq
R
).
#[
global
]
Instance
Rops
: (@
Ring_ops
R
0%
R
1%
R
Rplus
Rmult
Rminus
Ropp
(@
eq
R
)).
Defined
.
#[
global
]
Instance
Rri
: (
Ring
(
Ro
:=
Rops
)).
Defined
.
Class
can_compute_Z
(
z
:
Z
) :=
dummy_can_compute_Z
:
True
.
#[
global
]
Hint
Extern
0 (
can_compute_Z
?
v
) =>
match
isZcst
v
with
true
=>
exact
I
end
:
typeclass_instances
.
#[
global
]
Instance
reify_IZR
z
lvar
{
_
:
can_compute_Z
z
} :
reify
(
PEc
z
)
lvar
(
IZR
z
).
Defined
.
Lemma
R_one_zero
: 1%
R
<>
0%
R
.
#[
global
]
Instance
Rcri
: (
Cring
(
Rr
:=
Rri
)).
#[
global
]
Instance
Rdi
: (
Integral_domain
(
Rcr
:=
Rcri
)).