proposition: Lemma Cauchy_IR_opp_as_CR_opp : forall x:Cauchy_IR, (-Cauchy_IRasCR x == Cauchy_IRasCR ([--]x))%CR.
proof: Proof. intros [x Hx]. apply regFunEq_equiv, regFunEq_e. intros e. simpl. destruct (Hx (proj1_sig e) (Qpos_ispos e)) as [n1 Hn1]. destruct (CS_seq_inv Q_as_COrdField x Hx (proj1_sig e) (Qpos_ispos e)) as [n2 Hn2]. set (n:=(Nat.max n1 n2)). change (@ball Q_as_MetricSpace (proj1_sig e+proj1_sig e) (- x n1) (- x n2))%Q. apply (@ball_triangle Q_as_MetricSpace _ _ _ (- x n)%Q). simpl; unfold Qball. unfold QAbsSmall. setoid_replace (- x n1 - - x n)%Q with (x n - x n1)%Q. 2: ring. apply (Hn1 n). apply Nat.le_max_l. apply Hn2. apply Nat.le_max_r. 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