proposition: Lemma Qfloor_resp_le : forall x y, x <= y -> (Qfloor x <= Qfloor y)%Z.
proof: Proof. intros [xn xd] [yn yd] Hxy. unfold Qle in *. simpl in *. rewrite <- (Zdiv_mult_cancel_r xn (Zpos xd) (Zpos yd)); auto with *. rewrite <- (Zdiv_mult_cancel_r yn (Zpos yd) (Zpos xd)); auto with *. rewrite (Z.mul_comm (Zpos yd) (Zpos xd)). apply Z_div_le; auto with *. Qed.
imports: QArith