proposition: Lemma Qdiv_bounded_Zdiv (x y : Z) : 'Z.div x y ≤ ('x / 'y : Q) < 'Z.div x y + 1.
proof: Proof. rewrite Qround.Zdiv_Qdiv. split. now apply Qround.Qfloor_le. rewrite <-(rings.preserves_1 (f:=cast Z Q)). rewrite <-rings.preserves_plus. now apply Qround.Qlt_floor. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.Program.Program Coq.QArith.QArith Coq.ZArith.ZArith Bignums.BigZ.BigZ CoRN.model.totalorder.QposMinMax CoRN.metric2.MetricMorphisms CoRN.model.metric2.Qmetric CoRN.util.Qdlog CoRN.reals.faster.ARArith MathClasses.theory.int_pow MathClasses.theory.nat_pow MathClasses.interfaces.rationals MathClasses.implementations.stdlib_rationals MathClasses.interfaces.integers MathClasses.implementations.stdlib_binary_integers MathClasses.implementations.fast_integers MathClasses.implementations.dyadics