proposition: Lemma approximateQ_big : forall (z:Z) a p, ((z#1) <= a) -> (z#1) <= approximateQ a p.
proof: Proof. intros z [n d] p Ha. unfold approximateQ. unfold Qle in *. simpl in *. apply Zlt_succ_le. unfold Z.succ. apply Zmult_gt_0_lt_reg_r with (Zpos d). reflexivity. replace ((n * Zpos p / Zpos d * 1 + 1) * Zpos d)%Z with (Zpos d* (n*Zpos p/ Zpos d) + (Z.modulo (n*Zpos p) (Zpos d)) - (Z.modulo (n*Zpos p) (Zpos d)) + Zpos d)%Z by ring. rewrite <- (Z_div_mod_eq_full (n*Zpos p) (Zpos d)). apply Z.le_lt_trans with (n*1*Zpos p)%Z. replace (z*Zpos p*Zpos d)%Z with (z*Zpos d*Zpos p)%Z by ring. apply Zmult_lt_0_le_compat_r; auto with *. apply Zlt_0_minus_lt. replace (n * Zpos p - (n * Zpos p) mod (Zpos d) + Zpos d - n * 1 * Zpos p)%Z with (Zpos d - (Z.modulo (n*Zpos p) (Zpos d)))%Z by ring. rewrite <- Zlt_plus_swap. ring_simplify. assert (X:(Zpos d >0)%Z) by auto with *. destruct (Z_mod_lt (n*Zpos p) _ X). assumption. 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