proposition: Lemma approximateQ_correct : forall x p, ball (1#p) x (approximateQ x p).
proof: Proof. intros [n d] p. split; simpl; unfold Qle; simpl. - apply Z.le_trans with 0%Z. discriminate. apply Zmult_le_0_compat; auto with *. replace (n * Zpos p + - (n * Zpos p / Zpos d) * Zpos d)%Z with (n * Zpos p - ((n * Zpos p / Zpos d) * Zpos d))%Z by ring. apply Zle_minus_le_0. rewrite Zmult_comm. apply Z_mult_div_ge; auto with *. - rewrite Zpos_mult_morphism. apply Zmult_le_compat_r; auto with *. replace (n * Zpos p + - (n * Zpos p / Zpos d) * Zpos d)%Z with ((n*Zpos p) mod (Zpos d))%Z. destruct (Z_mod_lt (n*Zpos p) (Zpos d)); auto with *. symmetry. transitivity (n * Zpos p - (Zpos d*(n * Zpos p / Zpos d)))%Z;[ring|]. symmetry. apply -> Zeq_plus_swap. rewrite Zplus_comm. symmetry. apply Z_div_mod_eq_full. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.metric2.CRmetric CoRN.model.metric2.Qmetric Coq.ZArith.Zdiv