proposition: Lemma Cauchy_IR_plus_as_CR_plus : forall x y:Cauchy_IR, (Cauchy_IRasCR x + Cauchy_IRasCR y == Cauchy_IRasCR (x[+]y))%CR.
proof: Proof. intros [x Hx] [y Hy]. apply regFunEq_equiv, regFunEq_e. intros e. simpl. unfold Cap_raw. simpl. destruct (Hx (proj1_sig ((1 # 2) * e)%Qpos)) as [n1 Hn1]. destruct (Hy (proj1_sig ((1 # 2) * e)%Qpos)) as [n2 Hn2]. destruct (CS_seq_plus) as [n3 Hn3]. set (n:= Nat.max n3 (Nat.max n1 n2)). change (@ball Q_as_MetricSpace (proj1_sig e+proj1_sig e) (x n1 + y n2) (x n3 + y n3))%Q. apply ball_triangle with (x n + y n)%Q. assert (QposEq e (((1 # 2) * e +(1 # 2) * e))) by (unfold QposEq; simpl; ring). apply (ball_wd _ H _ _ (reflexivity _) _ _ (reflexivity _)). clear H. apply ball_triangle with (x n1 + y n)%Q; simpl; unfold Qball. unfold QAbsSmall. setoid_replace (x n1 + y n2 - (x n1 + y n))%Q with (y n2 - y n)%Q. 2: ring. apply AbsSmall_minus. apply Hn2. unfold n. rewrite Nat.max_assoc. auto with *. unfold QAbsSmall. setoid_replace (x n1 + y n - (x n + y n))%Q with (x n1 - x n)%Q. 2: ring. apply AbsSmall_minus. apply Hn1. unfold n. rewrite (Nat.max_comm n1). rewrite Nat.max_assoc. auto with *. eapply Hn3; 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