proposition: Lemma compress_raw_prop : forall x (e:Qpos), ball (proj1_sig e) x (Cunit (compress_raw x e)).
proof: Proof. intros x. intros [[n d] dpos]. destruct n as [|n|n]. inversion dpos. 2: inversion dpos. simpl. assert (0 < Z.succ (Zpos (d~0)%positive / Zpos n))%Z as zpos. { unfold Z.succ. apply (Z.lt_le_trans _ (0+1)). reflexivity. apply Z.add_le_mono_r. apply Z_div_pos. reflexivity. discriminate. } destruct (Z.succ (Zpos (xO d) / Zpos n)) eqn:Hp. - exfalso. discriminate. - apply ball_weak_le with (2#p). unfold Qle. simpl. rewrite Zpos_mult_morphism. rewrite <- Hp. unfold Z.succ. rewrite Zmult_plus_distr_r. apply Zle_0_minus_le. replace (Zpos n * (Zpos (d~0)%positive / Zpos n) + Zpos n * 1 - Zpos (d~0)%positive)%Z with (Zpos n - (Zpos (xO d) - Zpos n * (Zpos (xO d) / Zpos n)))%Z by ring. apply Zle_minus_le_0. replace (Zpos (d~0)%positive - Zpos n * (Zpos (d~0)%positive / Zpos n))%Z with (Zpos (xO d) mod (Zpos n))%Z. destruct (Z_mod_lt (Zpos (xO d)) (Zpos n)); auto with *. symmetry. transitivity (Zpos (xO d) - (Zpos n*(Zpos (xO d) / Zpos n)))%Z;[ring|]. symmetry; apply -> Zeq_plus_swap. rewrite Zplus_comm. symmetry. apply Z_div_mod_eq_full. assert (QposEq (2#p) ((1#p)+(1#p))). { unfold QposEq. simpl. repeat rewrite -> Qmake_Qdiv. unfold Qdiv. ring. } apply (ball_wd _ H _ _ (reflexivity _) _ _ (reflexivity _)). clear H. eapply ball_triangle with (Cunit (approximate x (Qpos2QposInf (1#p)))). apply ball_approx_r. Transparent CR. change (ball (m:=Complete Q_as_MetricSpace) (1 # p) (Cunit (approximate x (Qpos2QposInf (1 # p)))) (Cunit (approximateQ (approximate x (Qpos2QposInf (1 # p))) p))). rewrite -> ball_Cunit. apply approximateQ_correct. - exfalso. discriminate. 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