Library Coq.Reals.Rdefinitions
Definitions for the axiomatization
Require Export ZArith_base.
Parameter R :
Set.
Delimit Scope R_scope with R.
Open Local 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.