proposition: Lemma CRasCR : forall x:CR, (Cauchy_IRasCR (CRasCauchy_IR x)==x)%CR.
proof: Proof. intros x. apply regFunEq_equiv, regFunEq_e. intros e. simpl. destruct (CRasCauchy_IR_raw_is_Cauchy x (proj1_sig e) (Qpos_ispos e)) as [n Hn]. unfold CRasCauchy_IR_raw in *. apply ball_closed. intros d dpos. setoid_replace (proj1_sig e+proj1_sig e+d)%Q with (proj1_sig (e+(exist _ _ dpos+e))%Qpos) by (simpl; ring). destruct d as [dn dd]. destruct dn as [|dn|dn]. inversion dpos. 2: inversion dpos. apply ball_triangle with (approximate x (Qpos2QposInf (1#P_of_succ_nat (n+(nat_of_P dd)))))%Qpos. - apply ball_sym. eapply Hn;auto with *. - eapply ball_weak_le;[|apply regFun_prf]. simpl. eapply plus_resp_leEq;simpl. apply Qle_trans with (1#dd)%Q. change (dd <= P_of_succ_nat (n + nat_of_P dd))%Z. destruct n. simpl. rewrite P_of_succ_nat_o_nat_of_P_eq_succ. rewrite Pplus_one_succ_r. rewrite Zpos_plus_distr. auto with *. rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ. rewrite <- nat_of_P_plus_morphism. rewrite P_of_succ_nat_o_nat_of_P_eq_succ. rewrite Pplus_one_succ_r. repeat rewrite Zpos_plus_distr. rewrite <- Zplus_assoc. rewrite Zplus_comm. rewrite <- Zplus_assoc. rewrite <- Zpos_plus_distr. rewrite <- Pplus_one_succ_l. change (dd+0 <= dd + Pos.succ (P_of_succ_nat n))%Z. auto with *. change (dd <= dn*dd)%Z. auto with *. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.reals.Cauchy_IR CoRN.tactics.CornTac Coq(Lia) CoRN.model.metric2.Qmetric CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.reals.fast.CRFieldOps