proposition: Lemma QposCeiling_Qceiling (q: Qpos): (QposCeiling q: Z) = Qceiling q.
proof: Proof. Proof with auto with *. unfold QposCeiling. pose proof Qle_ceiling q. destruct (Qceiling q); try reflexivity; exfalso; destruct q; simpl in *. apply (Qlt_not_le 0 x q)... apply (Qlt_irrefl 0). apply Qlt_le_trans with x... apply Qle_trans with (Zneg p)... Qed.
imports: Coq.QArith.QArith Coq.QArith.Qpower CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields2 Coq.Logic.Eqdep_dec CoRN.tactics.CornTac Coq.QArith.Qround Coq.QArith.Qabs CoRN.stdlib_omissions.Q