proposition: Lemma Qle_ceiling : forall x, x <= Qceiling x.
proof: Proof. intros x. apply Qle_trans with (- - x). - rewrite Qopp_involutive. auto with *. - change (Qceiling x:Q) with (-(Qfloor(-x))). auto with *. Qed.
imports: QArith