proposition: Lemma Qceiling_lt : forall x, (Qceiling x-1)%Z < x.
proof: Proof. intros x. unfold Qceiling. replace (- Qfloor (- x) - 1)%Z with (-(Qfloor (-x) + 1))%Z by ring. change ((- (Qfloor (- x) + 1))%Z:Q) with (-(Qfloor (- x) + 1)%Z). apply Qlt_le_trans with (- - x); auto with *. rewrite Qopp_involutive. auto with *. Qed.
imports: QArith