Library Coq.Reals.Rdefinitions
Definitions for the axiomatization
Require
Export
ZArith_base
.
Parameter
R
:
Set
.
Delimit
Scope
R_scope
with
R
.
Local Open
Scope
R_scope
.
Parameter
R0
:
R
.
Parameter
R1
:
R
.
Parameter
Rplus
:
R
->
R
->
R
.
Parameter
Rmult
:
R
->
R
->
R
.
Parameter
Ropp
:
R
->
R
.
Parameter
Rinv
:
R
->
R
.
Parameter
Rlt
:
R
->
R
->
Prop
.
Parameter
up
:
R
->
Z
.
Infix
"
+" :=
Rplus
:
R_scope
.
Infix
"
*" :=
Rmult
:
R_scope
.
Notation
"
- x" := (
Ropp
x
) :
R_scope
.
Notation
"
/ x" := (
Rinv
x
) :
R_scope
.
Infix
"
<" :=
Rlt
:
R_scope
.
Definition
Rgt
(
r1
r2
:
R
) :
Prop
:=
r2
<
r1
.
Definition
Rle
(
r1
r2
:
R
) :
Prop
:=
r1
<
r2
\/
r1
=
r2
.
Definition
Rge
(
r1
r2
:
R
) :
Prop
:=
Rgt
r1
r2
\/
r1
=
r2
.
Definition
Rminus
(
r1
r2
:
R
) :
R
:=
r1
+
-
r2
.
Definition
Rdiv
(
r1
r2
:
R
) :
R
:=
r1
*
/
r2
.
Infix
"
-" :=
Rminus
:
R_scope
.
Infix
"
/" :=
Rdiv
:
R_scope
.
Infix
"
<=" :=
Rle
:
R_scope
.
Infix
"
>=" :=
Rge
:
R_scope
.
Infix
"
>" :=
Rgt
:
R_scope
.
Notation
"
x <= y <= z" := (
x
<=
y
/\
y
<=
z
) :
R_scope
.
Notation
"
x <= y < z" := (
x
<=
y
/\
y
<
z
) :
R_scope
.
Notation
"
x < y < z" := (
x
<
y
/\
y
<
z
) :
R_scope
.
Notation
"
x < y <= z" := (
x
<
y
/\
y
<=
z
) :
R_scope
.