proposition: Lemma CRasCauchy_IR_wd : forall (x y:CR), (x==y)%CR -> CRasCauchy_IR x[=]CRasCauchy_IR y.
proof: Proof. intros x y Hxy. eapply Eq_alt_2_2. intros e He. destruct e as [en ed]. destruct en as [|en|en]. inversion He. 2: inversion He. exists (pred(nat_of_P (2*ed))). intros m Hm. simpl. unfold CRasCauchy_IR_raw. set (d:=(1 # P_of_succ_nat m)%Qpos). change (ball (en#ed) (approximate x (Qpos2QposInf d)) (approximate y (Qpos2QposInf d))). eapply ball_weak_le;[|apply Hxy]. unfold d. simpl. ring_simplify. apply Qle_trans with ((2#1)*(1#(2 * ed)))%Q. eapply mult_resp_leEq_lft;try discriminate. change ((2*ed)<=P_of_succ_nat m)%Z. rewrite <- Zpos_mult_morphism. rewrite (anti_convert_pred_convert (2*ed)). do 2 rewrite <- POS_anti_convert. apply inj_le. auto with *. change (1#2*ed)%Q with ((1#2)*(1#ed))%Q. ring_simplify. 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