proposition: Lemma Qfloor_ball q: Qball (1#2) ((Qfloor q # 1) + (1#2)) q.
proof: Proof. Proof with auto with *. intros. apply Qball_Qabs. simpl. apply Qabs_case; intros. apply Q.Qplus_le_l with ((-1#2)%Q + q). ring_simplify. apply Qfloor_le. pose proof (Qlt_floor q). apply (Qplus_le_l _ _ ((1#2) + (Qfloor q # 1))). ring_simplify. apply Qlt_le_weak. rewrite inject_Z_plus in H0. apply H0. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.Prelength CoRN.metric2.Classification CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.QArith.Qabs CoRN.metric2.UniformContinuity MathClasses.implementations.stdlib_rationals Coq.QArith.Qround