Library Coq.Reals.Raxioms
Lifts of basic operations for classical reals
Field operations
Addition
Open Scope CReal_scope.
Lemma Rrepr_0 :
Rrepr 0
== 0.
Lemma Rrepr_1 :
Rrepr 1
== 1.
Lemma Rrepr_plus :
forall x y:
R,
Rrepr (
x + y)
== Rrepr x + Rrepr y.
Lemma Rrepr_opp :
forall x:
R,
Rrepr (
- x)
== - Rrepr x.
Lemma Rrepr_minus :
forall x y:
R,
Rrepr (
x - y)
== Rrepr x - Rrepr y.
Lemma Rrepr_mult :
forall x y:
R,
Rrepr (
x * y)
== Rrepr x * Rrepr y.
Lemma Rrepr_inv :
forall (
x:
R) (
xnz :
Rrepr x # 0),
Rrepr (
/ x)
== (/ Rrepr x) xnz.
Lemma Rrepr_le :
forall x y:
R, (
x <= y)%
R <-> Rrepr x <= Rrepr y.
Lemma Rrepr_appart :
forall x y:
R,
(
x <> y)%
R -> Rrepr x # Rrepr y.
Lemma Rappart_repr :
forall x y:
R,
Rrepr x # Rrepr y -> (
x <> y)%
R.
Close Scope CReal_scope.
Lemma Rplus_comm :
forall r1 r2:
R,
r1 + r2 = r2 + r1.
Hint Resolve Rplus_comm:
real.
Lemma Rplus_assoc :
forall r1 r2 r3:
R,
r1 + r2 + r3 = r1 + (r2 + r3).
Hint Resolve Rplus_assoc:
real.
Lemma Rplus_opp_r :
forall r:
R,
r + - r = 0.
Hint Resolve Rplus_opp_r:
real.
Lemma Rplus_0_l :
forall r:
R, 0
+ r = r.
Hint Resolve Rplus_0_l:
real.