Library Coq.QArith.Qround
Require Import QArith.
Import Zdiv.
Lemma Qopp_lt_compat:
forall p q :
Q,
p < q -> - q < - p.
Hint Resolve Qopp_lt_compat :
qarith.
Definition Qfloor (
x:
Q) :=
let (
n,
d) :=
x in Z.div 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.
Lemma Zdiv_Qdiv (
n m:
Z): (
n / m)%
Z = Qfloor (
n / m).