proposition: Lemma QposCeiling_Qceiling (q : Qpos) : Z.pos (QposCeiling (proj1_sig q)) = Qround.Qceiling (proj1_sig q).
proof: Proof. Proof with auto with qarith. unfold QposCeiling. destruct q as [q qpos]. simpl. pose proof Qround.Qle_ceiling q. destruct (Qround.Qceiling q); try reflexivity; exfalso; destruct q; simpl in *. exact (Qlt_not_le _ _ qpos H). apply (Qlt_not_le _ _ qpos). apply Qle_trans with (Zneg p)... Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.reals.CRreal CoRN.stdlib_omissions.List Coq.Unicode.Utf8 Coq.QArith.QArith Coq.QArith.Qabs CoRN.model.totalorder.QposMinMax CoRN.util.Qsums CoRN.model.metric2.Qmetric CoRN.model.setoids.Qsetoid CoRN.reals.fast.CRArith QnonNeg CoRN.util.Qgcd Coq.Program.Program CoRN.reals.fast.uneven_CRplus CoRN.stdlib_omissions.P CoRN.stdlib_omissions.Z CoRN.stdlib_omissions.Q CoRN.tactics.Qauto CoRN.ode.metric CoRN.ode.FromMetric2 MathClasses.implementations.stdlib_rationals