Require Import QArith.
Lemma Qopp_lt_compat:
forall p q :
Q,
p <
q -> -
q < -
p.
Hint Resolve Qopp_lt_compat :
qarith.
Coercion Local inject_Z :
Z >->
Q.
Definition Qfloor (
x:Q) :=
let (
n,d) :=
x in Zdiv n (
Zpos d).
Definition Qceiling (
x:Q) := (-(Qfloor (-x)))%Z.
Lemma Qfloor_Z :
forall z:Z,
Qfloor z =
z.
Lemma Qceiling_Z :
forall z:Z,
Qceiling z =
z.
Lemma Qfloor_le :
forall x,
Qfloor x <=
x.
Hint Resolve Qfloor_le :
qarith.
Lemma Qle_ceiling :
forall x,
x <=
Qceiling x.
Hint Resolve Qle_ceiling :
qarith.
Lemma Qle_floor_ceiling :
forall x,
Qfloor x <=
Qceiling x.
Lemma Qlt_floor :
forall x,
x < (
Qfloor x+1)%Z.
Hint Resolve Qlt_floor :
qarith.
Lemma Qceiling_lt :
forall x, (
Qceiling x-1)%Z <
x.
Hint Resolve Qceiling_lt :
qarith.
Lemma Qfloor_resp_le :
forall x y,
x <=
y -> (
Qfloor x <=
Qfloor y)%Z.
Hint Resolve Qfloor_resp_le :
qarith.
Lemma Qceiling_resp_le :
forall x y,
x <=
y -> (
Qceiling x <=
Qceiling y)%Z.
Hint Resolve Qceiling_resp_le :
qarith.
Add Morphism Qfloor with signature Qeq ==> @
eq _ as Qfloor_comp.
Add Morphism Qceiling with signature Qeq ==> @
eq _ as Qceiling_comp.