Library Coq.QArith.QArith_base
Definition of Q and basic properties
Rationals are pairs of
Z and
positive numbers.
a#b denotes the fraction a over b.
injection from Z is injective.
Another approach : using Qcompare for defining order relations.
In a word, Qeq is a setoid equality.
Furthermore, this equality is decidable:
Addition, multiplication and opposite
The addition, multiplication and opposite are defined
in the straightforward way:
A light notation for Zpos
Setoid compatibility results
0 and 1 are apart
Properties of Qadd
Addition is associative:
0 is a neutral element for addition:
Commutativity of addition:
Injectivity of addition (uses theory about Qopp above):
Properties of Qmult
Multiplication is associative:
multiplication and zero
1 is a neutral element for multiplication:
Commutativity of multiplication
Distributivity over Qadd
Integrality
inject_Z is a ring homomorphism:
Injectivity of Qmult (requires theory about Qinv above):
Properties of order upon Q.
Large = strict or equal
x<y iff ~(y<=x)
Some decidability results about orders.
Compatibility of operations with respect to order.
Lemma Qopp_le_compat :
forall p q,
p<=q -> -q <= -p.
Hint Resolve Qopp_le_compat :
qarith.
Lemma Qle_minus_iff :
forall p q,
p <= q <-> 0
<= q+-p.
Lemma Qlt_minus_iff :
forall p q,
p < q <-> 0
< q+-p.
Lemma Qplus_le_compat :
forall x y z t,
x<=y -> z<=t -> x+z <= y+t.
Open Scope Z_scope.
Close Scope Z_scope.
Lemma Qplus_lt_le_compat :
forall x y z t,
x<y -> z<=t -> x+z < y+t.
Open Scope Z_scope.
Close Scope Z_scope.
Lemma Qplus_le_l (
x y z:
Q):
x + z <= y + z <-> x <= y.
Lemma Qplus_le_r (
x y z:
Q):
z + x <= z + y <-> x <= y.
Lemma Qplus_lt_l (
x y z:
Q):
x + z < y + z <-> x < y.
Lemma Qplus_lt_r (
x y z:
Q):
z + x < z + y <-> x < y.
Lemma Qmult_le_compat_r :
forall x y z,
x <= y -> 0
<= z -> x*z <= y*z.
Open Scope Z_scope.
Close Scope Z_scope.
Lemma Qmult_lt_0_le_reg_r :
forall x y z, 0
< z -> x*z <= y*z -> x <= y.
Open Scope Z_scope.
Close Scope Z_scope.
Lemma Qmult_le_r (
x y z:
Q): 0
< z -> (x*z <= y*z <-> x <= y).
Lemma Qmult_le_l (
x y z:
Q): 0
< z -> (z*x <= z*y <-> x <= y).
Lemma Qmult_lt_compat_r :
forall x y z, 0
< z -> x < y -> x*z < y*z.
Open Scope Z_scope.
Close Scope Z_scope.
Lemma Qmult_lt_r:
forall x y z, 0
< z -> (x*z < y*z <-> x < y).
Open Scope Z_scope.
Close Scope Z_scope.
Lemma Qmult_lt_l (
x y z:
Q): 0
< z -> (z*x < z*y <-> x < y).
Lemma Qmult_le_0_compat :
forall a b, 0
<= a -> 0
<= b -> 0
<= a*b.
Lemma Qinv_le_0_compat :
forall a, 0
<= a -> 0
<= /a.
Lemma Qle_shift_div_l :
forall a b c,
0
< c -> a*c <= b -> a <= b/c.
Lemma Qle_shift_inv_l :
forall a c,
0
< c -> a*c <= 1
-> a <= /c.
Lemma Qle_shift_div_r :
forall a b c,
0
< b -> a <= c*b -> a/b <= c.
Lemma Qle_shift_inv_r :
forall b c,
0
< b -> 1
<= c*b -> /b <= c.
Lemma Qinv_lt_0_compat :
forall a, 0
< a -> 0
< /a.
Lemma Qlt_shift_div_l :
forall a b c,
0
< c -> a*c < b -> a < b/c.
Lemma Qlt_shift_inv_l :
forall a c,
0
< c -> a*c < 1
-> a < /c.
Lemma Qlt_shift_div_r :
forall a b c,
0
< b -> a < c*b -> a/b < c.
Lemma Qlt_shift_inv_r :
forall b c,
0
< b -> 1
< c*b -> /b < c.
Lemma Qinv_lt_contravar :
forall a b :
Q,
0
< a -> 0
< b -> (a < b <-> /b < /a).
Rational to the n-th power