# Library floor

``` Require Import misc. Require Import Q_misc. Require Import QArith. Require Import ZArith. Require Import Qround. Definition Z_of_positive (x:positive) := Zpos x. Definition fl (x:Q) : Z := Qfloor x. Lemma fl_def:   forall x: Q,     fl x <= x /\ x < fl x + 1. Proof.   intros.   split.     apply Qfloor_le.     assert (H_aux: fl x + 1 == (fl x + 1)%Z).       unfold Qeq, Qplus, Q_of_nat; simpl; ring_simplify; auto.     rewrite H_aux; clear H_aux.     apply Qlt_floor. Qed. Lemma fl_integerp:   forall x: Q, fl x == x <-> in_Z x. Proof.   intros.   split.     intros.     unfold in_Z.     exists (fl x).     auto with qarith.     intros H_in_Z.     elim H_in_Z.     intros x' H_x.     rewrite H_x.     rewrite Qfloor_Z.     auto with qarith. Qed. Axiom fl_minus_in_Z:   forall x: Q,   forall H_in_Z: in_Z x,   fl (- x) = (- (fl x))%Z. Axiom fl_minus_not_in_Z:   forall x: Q,   forall H_not_in_Z: ~ in_Z x,   fl (- x) = (- (fl x) - 1)%Z. Axiom fl_m_n:   forall x: Q,   ( fl (-x) = - fl ((x - (1#Qden(x)))%Q) - 1)%Z. Lemma fl_monotone_linear:   forall x y : Q,   x <= y -> (fl x <= fl y)%Z. Proof.   intros.   apply Qfloor_resp_le.   assumption. Qed. Axiom n_le_fl_linear:   forall x: Q,   forall n: Z,   n <= x -> (n <= fl x)%Z. Axiom fl_plus_int_rewrite:   forall x: Q,   forall n: Z,   (fl (x + n) = fl x + n)%Z. Axiom fl_div_int_rewrite:   forall x: Q,   forall n: Z,   forall H_n_pos: (n > 0)%Z,   (fl (fl x / n) == fl (x / n))%Z. Definition cg (x: Q) : Z := Qceiling x. Lemma cg_def_linear:   forall x: Q,   (cg x - 1%Z)%Z < x /\ x <= cg x. Proof.   intros; split; auto with qarith. Qed. Lemma cg_integerp:   forall x: Q, cg x == x <-> in_Z x. Proof.   intros.   split.     intros.     unfold in_Z.     exists (cg x).     auto with qarith.     intros H_in_Z.     elim H_in_Z.     intros x' H_x.     rewrite H_x.     unfold cg.     rewrite Qceiling_Z.     auto with qarith. Qed. Property cg_monotone_linear:   forall x y : Q,   x <= y -> (cg x <= cg y)%Z. Proof.   intros.   unfold cg, Qceiling.   apply Zle_left_rev.   rewrite Zopp_involutive.   rewrite Zplus_comm.   apply Zle_left.   apply Qfloor_resp_le.   auto with qarith. Qed. Axiom n_ge_cg_linear:   forall x: Q,   forall n: Z,   n >= x -> (n >= cg x)%Z. Axiom cg_plus_int_rewrite:   forall x: Q,   forall n: Z,   (cg (x + n) = cg x + n)%Z. Axiom cg_div_int_rewrite:   forall x: Q,   forall n: Z,   forall H_n_pos: (n > 0)%Z,   (cg (cg x / n) = cg (x / n))%Z. Lemma fl_cg_in_Z:   forall x: Q,   forall H_in_Z: in_Z x,   (cg x = fl x)%Z. Proof.   intros.   unfold cg, Qceiling.   fold (fl ( -x)).   rewrite (fl_minus_in_Z x).   ring.   assumption. Qed. Lemma fl_cg_not_in_Z:   forall x: Q,   forall H_not_in_Z: ~ in_Z x,   (cg x = fl x + 1%Z)%Z. Proof.   intros.   unfold cg, Qceiling.   fold (fl ( -x)).   rewrite (fl_minus_not_in_Z x).   ring.   assumption. Qed. Axiom fl_rewrite:   forall x y: Q,   x == y -> fl x = fl y. Lemma cg_rewrite:   forall x y: Q,   x == y -> cg x = cg y. Proof.   intros.   unfold cg, Qceiling.   fold (fl (- x)).   fold (fl (- y)).   assert (H_cc: (fl (- x))%Z = (fl (- y))%Z).     apply fl_rewrite.     apply Qopp_comp.     assumption.   auto with zarith. Qed. ```