Library Coq.Reals.Cauchy.ConstructiveCauchyReals
Require Import QArith.
Require Import Qabs.
Require Import Qround.
Require Import Logic.ConstructiveEpsilon.
Require CMorphisms.
The constructive Cauchy real numbers, ie the Cauchy sequences
of rational numbers.
Cauchy reals are Cauchy sequences of rational numbers,
equipped with explicit moduli of convergence and
an equivalence relation (the difference converges to zero).
Without convergence moduli, we would fail to prove that a Cauchy
sequence of constructive reals converges.
Because of the Specker sequences (increasing, computable
and bounded sequences of rationals that do not converge
to a computable real number), constructive reals do not
follow the least upper bound principle.
The double quantification on p q is needed to avoid
forall un, QSeqEquiv un (fun _ => un O) (fun q => O)
which says nothing about the limit of un.
We define sequences as positive -> Q instead of nat -> Q,
so that we can compute arguments like 2^n fast.
WARNING: this module is not meant to be imported directly,
please import `Reals.Abstract.ConstructiveReals` instead.
WARNING: this file is experimental and likely to change in future releases.
Definition QCauchySeq (un : positive -> Q)
: Prop
:= forall (k : positive) (p q : positive),
Pos.le k p
-> Pos.le k q
-> Qlt (Qabs (un p - un q)) (1 # k).
Definition CReal : Set
:= { x : (positive -> Q) | QCauchySeq x }.
Delimit Scope CReal_scope with CReal.
Local Open Scope CReal_scope.
Definition CRealLt (x y : CReal) : Set
:= { n : positive | Qlt (2 # n) (proj1_sig y n - proj1_sig x n) }.
Definition CRealLtProp (x y : CReal) : Prop
:= exists n : positive, Qlt (2 # n) (proj1_sig y n - proj1_sig x n).
Definition CRealGt (x y : CReal) := CRealLt y x.
Definition CReal_appart (x y : CReal) := sum (CRealLt x y) (CRealLt y x).
Infix "<" := CRealLt : CReal_scope.
Infix ">" := CRealGt : CReal_scope.
Infix "#" := CReal_appart : CReal_scope.
Lemma CRealLtEpsilon : forall x y : CReal,
CRealLtProp x y -> x < y.
Lemma CRealLtForget : forall x y : CReal,
x < y -> CRealLtProp x y.
Lemma CRealLt_lpo_dec : forall x y : CReal,
(forall (P : nat -> Prop), (forall n:nat, {P n} + {~P n})
-> {n | ~P n} + {forall n, P n})
-> CRealLt x y + (CRealLt x y -> False).
Definition CRealLe (x y : CReal) : Prop
:= CRealLt y x -> False.
Definition CRealGe (x y : CReal) := CRealLe y x.
Infix "<=" := CRealLe : CReal_scope.
Infix ">=" := CRealGe : CReal_scope.
Notation "x <= y <= z" := (x <= y /\ y <= z) : CReal_scope.
Notation "x <= y < z" := (prod (x <= y) (y < z)) : CReal_scope.
Notation "x < y < z" := (prod (x < y) (y < z)) : CReal_scope.
Notation "x < y <= z" := (prod (x < y) (y <= z)) : CReal_scope.
Definition CRealEq (x y : CReal) : Prop
:= (CRealLe y x) /\ (CRealLe x y).
Infix "==" := CRealEq : CReal_scope.
Lemma CRealLe_not_lt : forall x y : CReal,
(forall n:positive, Qle (proj1_sig x n - proj1_sig y n) (2 # n))
<-> x <= y.
Lemma CRealEq_diff : forall (x y : CReal),
CRealEq x y
<-> forall n:positive, Qle (Qabs (proj1_sig x n - proj1_sig y n)) (2 # n).
Lemma CRealLt_aboveSig : forall (x y : CReal) (n : positive),
(Qlt (2 # n)
(proj1_sig y n - proj1_sig x n))
-> let (k, _) := Qarchimedean (/(proj1_sig y n - proj1_sig x n - (2#n)))
in forall p:positive,
Pos.le (Pos.max n (2*k)) p
-> Qlt (2 # (Pos.max n (2*k)))
(proj1_sig y p - proj1_sig x p).
Lemma CRealLt_above : forall (x y : CReal),
CRealLt x y
-> { k : positive | forall p:positive,
Pos.le k p -> Qlt (2 # k) (proj1_sig y p - proj1_sig x p) }.
Lemma CRealLt_above_same : forall (x y : CReal) (n : positive),
Qlt (2 # n)
(proj1_sig y n - proj1_sig x n)
-> forall p:positive, Pos.le n p -> Qlt (proj1_sig x p) (proj1_sig y p).
Lemma CRealLt_asym : forall x y : CReal, x < y -> x <= y.
Lemma CRealLt_irrefl : forall x:CReal, x < x -> False.
Lemma CRealLe_refl : forall x : CReal, x <= x.
Lemma CRealEq_refl : forall x : CReal, x == x.
Lemma CRealEq_sym : forall x y : CReal, CRealEq x y -> CRealEq y x.
Lemma CRealLt_dec : forall x y z : CReal,
x < y -> sum (x < z) (z < y).
Definition linear_order_T x y z := CRealLt_dec x z y.
Lemma CReal_le_lt_trans : forall x y z : CReal,
x <= y -> y < z -> x < z.
Lemma CReal_lt_le_trans : forall x y z : CReal,
x < y -> y <= z -> x < z.
Lemma CReal_le_trans : forall x y z : CReal,
x <= y -> y <= z -> x <= z.
Lemma CReal_lt_trans : forall x y z : CReal,
x < y -> y < z -> x < z.
Lemma CRealEq_trans : forall x y z : CReal,
CRealEq x y -> CRealEq y z -> CRealEq x z.
Add Parametric Relation : CReal CRealEq
reflexivity proved by CRealEq_refl
symmetry proved by CRealEq_sym
transitivity proved by CRealEq_trans
as CRealEq_rel.
Instance CRealEq_relT : CRelationClasses.Equivalence CRealEq.
Instance CRealLt_morph
: CMorphisms.Proper
(CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRelationClasses.iffT)) CRealLt.
Instance CRealGt_morph
: CMorphisms.Proper
(CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRelationClasses.iffT)) CRealGt.
Instance CReal_appart_morph
: CMorphisms.Proper
(CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRelationClasses.iffT)) CReal_appart.
Add Parametric Morphism : CRealLtProp
with signature CRealEq ==> CRealEq ==> iff
as CRealLtProp_morph.
Add Parametric Morphism : CRealLe
with signature CRealEq ==> CRealEq ==> iff
as CRealLe_morph.
Add Parametric Morphism : CRealGe
with signature CRealEq ==> CRealEq ==> iff
as CRealGe_morph.
Lemma CRealLt_proper_l : forall x y z : CReal,
CRealEq x y
-> CRealLt x z -> CRealLt y z.
Lemma CRealLt_proper_r : forall x y z : CReal,
CRealEq x y
-> CRealLt z x -> CRealLt z y.
Lemma CRealLe_proper_l : forall x y z : CReal,
CRealEq x y
-> CRealLe x z -> CRealLe y z.
Lemma CRealLe_proper_r : forall x y z : CReal,
CRealEq x y
-> CRealLe z x -> CRealLe z y.
Lemma ConstCauchy : forall q : Q, QCauchySeq (fun _ => q).
Definition inject_Q : Q -> CReal.
Definition inject_Z : Z -> CReal
:= fun n => inject_Q (n # 1).
Notation "0" := (inject_Q 0) : CReal_scope.
Notation "1" := (inject_Q 1) : CReal_scope.
Notation "2" := (inject_Q 2) : CReal_scope.
Lemma CRealLt_0_1 : CRealLt (inject_Q 0) (inject_Q 1).
Lemma CReal_injectQPos : forall q : Q,
Qlt 0 q -> CRealLt (inject_Q 0) (inject_Q q).
Lemma CRealLtQ : forall (x : CReal) (q : Q),
CRealLt x (inject_Q q)
-> forall p:positive, Qlt (proj1_sig x p) (q + (1#p)).
Lemma CRealLtQopp : forall (x : CReal) (q : Q),
CRealLt (inject_Q q) x
-> forall p:positive, Qlt (q - (1#p)) (proj1_sig x p).
Lemma inject_Q_compare : forall (x : CReal) (p : positive),
x <= inject_Q (proj1_sig x p + (1#p)).
Add Parametric Morphism : inject_Q
with signature Qeq ==> CRealEq
as inject_Q_morph.
Instance inject_Q_morph_T
: CMorphisms.Proper
(CMorphisms.respectful Qeq CRealEq) inject_Q.
Lemma CReal_plus_cauchy
: forall (x y : CReal),
QCauchySeq (fun n : positive => Qred (proj1_sig x (2 * n)%positive
+ proj1_sig y (2 * n)%positive)).
Definition CReal_plus (x y : CReal) : CReal
:= exist _ (fun n : positive => Qred (proj1_sig x (2 * n)%positive
+ proj1_sig y (2 * n)%positive))
(CReal_plus_cauchy x y).
Infix "+" := CReal_plus : CReal_scope.
Definition CReal_opp (x : CReal) : CReal.
Notation "- x" := (CReal_opp x) : CReal_scope.
Definition CReal_minus (x y : CReal) : CReal
:= CReal_plus x (CReal_opp y).
Infix "-" := CReal_minus : CReal_scope.
Lemma belowMultiple : forall n p : positive, Pos.le n (p * n).
Lemma CReal_plus_assoc : forall (x y z : CReal),
(x + y) + z == x + (y + z).
Lemma CReal_plus_comm : forall x y : CReal,
x + y == y + x.
Lemma CReal_plus_0_l : forall r : CReal,
inject_Q 0 + r == r.
Lemma CReal_plus_0_r : forall r : CReal,
r + 0 == r.
Lemma CReal_plus_lt_compat_l :
forall x y z : CReal, y < z -> x + y < x + z.
Lemma CReal_plus_lt_compat_r :
forall x y z : CReal, y < z -> y + x < z + x.
Lemma CReal_plus_lt_reg_l :
forall x y z : CReal, x + y < x + z -> y < z.
Lemma CReal_plus_lt_reg_r :
forall x y z : CReal, y + x < z + x -> y < z.
Lemma CReal_plus_le_reg_l :
forall x y z : CReal, x + y <= x + z -> y <= z.
Lemma CReal_plus_le_reg_r :
forall x y z : CReal, y + x <= z + x -> y <= z.
Lemma CReal_plus_le_compat_l : forall r r1 r2, r1 <= r2 -> r + r1 <= r + r2.
Lemma CReal_plus_le_lt_compat :
forall r1 r2 r3 r4 : CReal, r1 <= r2 -> r3 < r4 -> r1 + r3 < r2 + r4.
Lemma CReal_plus_le_compat :
forall r1 r2 r3 r4 : CReal, r1 <= r2 -> r3 <= r4 -> r1 + r3 <= r2 + r4.
Lemma CReal_plus_opp_r : forall x : CReal,
x + - x == 0.
Lemma CReal_plus_opp_l : forall x : CReal,
- x + x == 0.
Lemma CReal_plus_proper_r : forall x y z : CReal,
CRealEq x y -> CRealEq (CReal_plus x z) (CReal_plus y z).
Lemma CReal_plus_proper_l : forall x y z : CReal,
CRealEq x y -> CRealEq (CReal_plus z x) (CReal_plus z y).
Add Parametric Morphism : CReal_plus
with signature CRealEq ==> CRealEq ==> CRealEq
as CReal_plus_morph.
Instance CReal_plus_morph_T
: CMorphisms.Proper
(CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRealEq)) CReal_plus.
Lemma CReal_plus_eq_reg_l : forall (r r1 r2 : CReal),
r + r1 == r + r2 -> r1 == r2.
Lemma CReal_opp_0 : -0 == 0.
Lemma CReal_opp_plus_distr : forall r1 r2, - (r1 + r2) == - r1 + - r2.
Lemma CReal_opp_involutive : forall x:CReal, --x == x.
Lemma CReal_opp_gt_lt_contravar : forall r1 r2, r1 > r2 -> - r1 < - r2.
Lemma CReal_opp_ge_le_contravar : forall r1 r2, r1 >= r2 -> - r1 <= - r2.
Lemma inject_Q_plus : forall q r : Q,
inject_Q (q + r) == inject_Q q + inject_Q r.
Lemma inject_Q_one : inject_Q 1 == 1.
Lemma inject_Q_lt : forall q r : Q,
Qlt q r -> inject_Q q < inject_Q r.
Lemma opp_inject_Q : forall q : Q,
inject_Q (-q) == - inject_Q q.
Lemma lt_inject_Q : forall q r : Q,
inject_Q q < inject_Q r -> Qlt q r.
Lemma le_inject_Q : forall q r : Q,
inject_Q q <= inject_Q r -> Qle q r.
Lemma inject_Q_le : forall q r : Q,
Qle q r -> inject_Q q <= inject_Q r.
Lemma inject_Z_plus : forall q r : Z,
inject_Z (q + r) == inject_Z q + inject_Z r.
Lemma opp_inject_Z : forall n : Z,
inject_Z (-n) == - inject_Z n.
: Prop
:= forall (k : positive) (p q : positive),
Pos.le k p
-> Pos.le k q
-> Qlt (Qabs (un p - un q)) (1 # k).
Definition CReal : Set
:= { x : (positive -> Q) | QCauchySeq x }.
Delimit Scope CReal_scope with CReal.
Local Open Scope CReal_scope.
Definition CRealLt (x y : CReal) : Set
:= { n : positive | Qlt (2 # n) (proj1_sig y n - proj1_sig x n) }.
Definition CRealLtProp (x y : CReal) : Prop
:= exists n : positive, Qlt (2 # n) (proj1_sig y n - proj1_sig x n).
Definition CRealGt (x y : CReal) := CRealLt y x.
Definition CReal_appart (x y : CReal) := sum (CRealLt x y) (CRealLt y x).
Infix "<" := CRealLt : CReal_scope.
Infix ">" := CRealGt : CReal_scope.
Infix "#" := CReal_appart : CReal_scope.
Lemma CRealLtEpsilon : forall x y : CReal,
CRealLtProp x y -> x < y.
Lemma CRealLtForget : forall x y : CReal,
x < y -> CRealLtProp x y.
Lemma CRealLt_lpo_dec : forall x y : CReal,
(forall (P : nat -> Prop), (forall n:nat, {P n} + {~P n})
-> {n | ~P n} + {forall n, P n})
-> CRealLt x y + (CRealLt x y -> False).
Definition CRealLe (x y : CReal) : Prop
:= CRealLt y x -> False.
Definition CRealGe (x y : CReal) := CRealLe y x.
Infix "<=" := CRealLe : CReal_scope.
Infix ">=" := CRealGe : CReal_scope.
Notation "x <= y <= z" := (x <= y /\ y <= z) : CReal_scope.
Notation "x <= y < z" := (prod (x <= y) (y < z)) : CReal_scope.
Notation "x < y < z" := (prod (x < y) (y < z)) : CReal_scope.
Notation "x < y <= z" := (prod (x < y) (y <= z)) : CReal_scope.
Definition CRealEq (x y : CReal) : Prop
:= (CRealLe y x) /\ (CRealLe x y).
Infix "==" := CRealEq : CReal_scope.
Lemma CRealLe_not_lt : forall x y : CReal,
(forall n:positive, Qle (proj1_sig x n - proj1_sig y n) (2 # n))
<-> x <= y.
Lemma CRealEq_diff : forall (x y : CReal),
CRealEq x y
<-> forall n:positive, Qle (Qabs (proj1_sig x n - proj1_sig y n)) (2 # n).
Lemma CRealLt_aboveSig : forall (x y : CReal) (n : positive),
(Qlt (2 # n)
(proj1_sig y n - proj1_sig x n))
-> let (k, _) := Qarchimedean (/(proj1_sig y n - proj1_sig x n - (2#n)))
in forall p:positive,
Pos.le (Pos.max n (2*k)) p
-> Qlt (2 # (Pos.max n (2*k)))
(proj1_sig y p - proj1_sig x p).
Lemma CRealLt_above : forall (x y : CReal),
CRealLt x y
-> { k : positive | forall p:positive,
Pos.le k p -> Qlt (2 # k) (proj1_sig y p - proj1_sig x p) }.
Lemma CRealLt_above_same : forall (x y : CReal) (n : positive),
Qlt (2 # n)
(proj1_sig y n - proj1_sig x n)
-> forall p:positive, Pos.le n p -> Qlt (proj1_sig x p) (proj1_sig y p).
Lemma CRealLt_asym : forall x y : CReal, x < y -> x <= y.
Lemma CRealLt_irrefl : forall x:CReal, x < x -> False.
Lemma CRealLe_refl : forall x : CReal, x <= x.
Lemma CRealEq_refl : forall x : CReal, x == x.
Lemma CRealEq_sym : forall x y : CReal, CRealEq x y -> CRealEq y x.
Lemma CRealLt_dec : forall x y z : CReal,
x < y -> sum (x < z) (z < y).
Definition linear_order_T x y z := CRealLt_dec x z y.
Lemma CReal_le_lt_trans : forall x y z : CReal,
x <= y -> y < z -> x < z.
Lemma CReal_lt_le_trans : forall x y z : CReal,
x < y -> y <= z -> x < z.
Lemma CReal_le_trans : forall x y z : CReal,
x <= y -> y <= z -> x <= z.
Lemma CReal_lt_trans : forall x y z : CReal,
x < y -> y < z -> x < z.
Lemma CRealEq_trans : forall x y z : CReal,
CRealEq x y -> CRealEq y z -> CRealEq x z.
Add Parametric Relation : CReal CRealEq
reflexivity proved by CRealEq_refl
symmetry proved by CRealEq_sym
transitivity proved by CRealEq_trans
as CRealEq_rel.
Instance CRealEq_relT : CRelationClasses.Equivalence CRealEq.
Instance CRealLt_morph
: CMorphisms.Proper
(CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRelationClasses.iffT)) CRealLt.
Instance CRealGt_morph
: CMorphisms.Proper
(CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRelationClasses.iffT)) CRealGt.
Instance CReal_appart_morph
: CMorphisms.Proper
(CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRelationClasses.iffT)) CReal_appart.
Add Parametric Morphism : CRealLtProp
with signature CRealEq ==> CRealEq ==> iff
as CRealLtProp_morph.
Add Parametric Morphism : CRealLe
with signature CRealEq ==> CRealEq ==> iff
as CRealLe_morph.
Add Parametric Morphism : CRealGe
with signature CRealEq ==> CRealEq ==> iff
as CRealGe_morph.
Lemma CRealLt_proper_l : forall x y z : CReal,
CRealEq x y
-> CRealLt x z -> CRealLt y z.
Lemma CRealLt_proper_r : forall x y z : CReal,
CRealEq x y
-> CRealLt z x -> CRealLt z y.
Lemma CRealLe_proper_l : forall x y z : CReal,
CRealEq x y
-> CRealLe x z -> CRealLe y z.
Lemma CRealLe_proper_r : forall x y z : CReal,
CRealEq x y
-> CRealLe z x -> CRealLe z y.
Lemma ConstCauchy : forall q : Q, QCauchySeq (fun _ => q).
Definition inject_Q : Q -> CReal.
Definition inject_Z : Z -> CReal
:= fun n => inject_Q (n # 1).
Notation "0" := (inject_Q 0) : CReal_scope.
Notation "1" := (inject_Q 1) : CReal_scope.
Notation "2" := (inject_Q 2) : CReal_scope.
Lemma CRealLt_0_1 : CRealLt (inject_Q 0) (inject_Q 1).
Lemma CReal_injectQPos : forall q : Q,
Qlt 0 q -> CRealLt (inject_Q 0) (inject_Q q).
Lemma CRealLtQ : forall (x : CReal) (q : Q),
CRealLt x (inject_Q q)
-> forall p:positive, Qlt (proj1_sig x p) (q + (1#p)).
Lemma CRealLtQopp : forall (x : CReal) (q : Q),
CRealLt (inject_Q q) x
-> forall p:positive, Qlt (q - (1#p)) (proj1_sig x p).
Lemma inject_Q_compare : forall (x : CReal) (p : positive),
x <= inject_Q (proj1_sig x p + (1#p)).
Add Parametric Morphism : inject_Q
with signature Qeq ==> CRealEq
as inject_Q_morph.
Instance inject_Q_morph_T
: CMorphisms.Proper
(CMorphisms.respectful Qeq CRealEq) inject_Q.
Lemma CReal_plus_cauchy
: forall (x y : CReal),
QCauchySeq (fun n : positive => Qred (proj1_sig x (2 * n)%positive
+ proj1_sig y (2 * n)%positive)).
Definition CReal_plus (x y : CReal) : CReal
:= exist _ (fun n : positive => Qred (proj1_sig x (2 * n)%positive
+ proj1_sig y (2 * n)%positive))
(CReal_plus_cauchy x y).
Infix "+" := CReal_plus : CReal_scope.
Definition CReal_opp (x : CReal) : CReal.
Notation "- x" := (CReal_opp x) : CReal_scope.
Definition CReal_minus (x y : CReal) : CReal
:= CReal_plus x (CReal_opp y).
Infix "-" := CReal_minus : CReal_scope.
Lemma belowMultiple : forall n p : positive, Pos.le n (p * n).
Lemma CReal_plus_assoc : forall (x y z : CReal),
(x + y) + z == x + (y + z).
Lemma CReal_plus_comm : forall x y : CReal,
x + y == y + x.
Lemma CReal_plus_0_l : forall r : CReal,
inject_Q 0 + r == r.
Lemma CReal_plus_0_r : forall r : CReal,
r + 0 == r.
Lemma CReal_plus_lt_compat_l :
forall x y z : CReal, y < z -> x + y < x + z.
Lemma CReal_plus_lt_compat_r :
forall x y z : CReal, y < z -> y + x < z + x.
Lemma CReal_plus_lt_reg_l :
forall x y z : CReal, x + y < x + z -> y < z.
Lemma CReal_plus_lt_reg_r :
forall x y z : CReal, y + x < z + x -> y < z.
Lemma CReal_plus_le_reg_l :
forall x y z : CReal, x + y <= x + z -> y <= z.
Lemma CReal_plus_le_reg_r :
forall x y z : CReal, y + x <= z + x -> y <= z.
Lemma CReal_plus_le_compat_l : forall r r1 r2, r1 <= r2 -> r + r1 <= r + r2.
Lemma CReal_plus_le_lt_compat :
forall r1 r2 r3 r4 : CReal, r1 <= r2 -> r3 < r4 -> r1 + r3 < r2 + r4.
Lemma CReal_plus_le_compat :
forall r1 r2 r3 r4 : CReal, r1 <= r2 -> r3 <= r4 -> r1 + r3 <= r2 + r4.
Lemma CReal_plus_opp_r : forall x : CReal,
x + - x == 0.
Lemma CReal_plus_opp_l : forall x : CReal,
- x + x == 0.
Lemma CReal_plus_proper_r : forall x y z : CReal,
CRealEq x y -> CRealEq (CReal_plus x z) (CReal_plus y z).
Lemma CReal_plus_proper_l : forall x y z : CReal,
CRealEq x y -> CRealEq (CReal_plus z x) (CReal_plus z y).
Add Parametric Morphism : CReal_plus
with signature CRealEq ==> CRealEq ==> CRealEq
as CReal_plus_morph.
Instance CReal_plus_morph_T
: CMorphisms.Proper
(CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRealEq)) CReal_plus.
Lemma CReal_plus_eq_reg_l : forall (r r1 r2 : CReal),
r + r1 == r + r2 -> r1 == r2.
Lemma CReal_opp_0 : -0 == 0.
Lemma CReal_opp_plus_distr : forall r1 r2, - (r1 + r2) == - r1 + - r2.
Lemma CReal_opp_involutive : forall x:CReal, --x == x.
Lemma CReal_opp_gt_lt_contravar : forall r1 r2, r1 > r2 -> - r1 < - r2.
Lemma CReal_opp_ge_le_contravar : forall r1 r2, r1 >= r2 -> - r1 <= - r2.
Lemma inject_Q_plus : forall q r : Q,
inject_Q (q + r) == inject_Q q + inject_Q r.
Lemma inject_Q_one : inject_Q 1 == 1.
Lemma inject_Q_lt : forall q r : Q,
Qlt q r -> inject_Q q < inject_Q r.
Lemma opp_inject_Q : forall q : Q,
inject_Q (-q) == - inject_Q q.
Lemma lt_inject_Q : forall q r : Q,
inject_Q q < inject_Q r -> Qlt q r.
Lemma le_inject_Q : forall q r : Q,
inject_Q q <= inject_Q r -> Qle q r.
Lemma inject_Q_le : forall q r : Q,
Qle q r -> inject_Q q <= inject_Q r.
Lemma inject_Z_plus : forall q r : Z,
inject_Z (q + r) == inject_Z q + inject_Z r.
Lemma opp_inject_Z : forall n : Z,
inject_Z (-n) == - inject_Z n.