proposition: Lemma Cauchy_IRasCR_wd : forall (x y:Cauchy_IR), x[=]y -> (Cauchy_IRasCR x==Cauchy_IRasCR y)%CR.
proof: Proof. intros [x Hx] [y Hy] Hxy. apply regFunEq_equiv, regFunEq_e. intros e. apply ball_closed. intros d dpos. simpl. destruct (Hx (proj1_sig e) (Qpos_ispos e)) as [a Ha]. destruct (Hy (proj1_sig e) (Qpos_ispos e)) as [b Hb]. destruct (Eq_alt_2_1 _ _ _ Hxy _ dpos) as [c Hc]. simpl in Hc. unfold Qball. set (n:= Nat.max (Nat.max a b) c). unfold QAbsSmall. setoid_replace (x a - y b)%Q with ((x a - x n) + (y n - y b) + (x n - y n))%Q. 2: ring. autorewrite with QposElim. repeat (eapply AbsSmall_plus). apply AbsSmall_minus. apply Ha;unfold n;apply Nat.le_trans with (Nat.max a b); auto with *. apply Hb; unfold n;apply Nat.le_trans with (Nat.max a b); auto with *. apply Hc; unfold n;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