proposition: Lemma Cauchy_IR_inv_as_CR_inv_short : forall (x:Cauchy_IR) x_, (@CRinvT (Cauchy_IRasCR x) (Cauchy_IR_nonZero_as_CR_nonZero_1 _ x_) == Cauchy_IRasCR (f_rcpcl x x_))%CR.
proof: Proof. intros [x Hx] [H|H]. set (x':=(Build_CauchySeq Q_as_COrdField x Hx)) in *. assert (H':(cm_unit Cauchy_IR)[<][--](x':Cauchy_IR)). apply inv_cancel_less. rstepl x'. assumption. set (y:= (Cauchy_IRasCR [--](f_rcpcl (F:=Cauchy_IR) ([--](x':Cauchy_IR)) (@inr _ _ H')))%CR). transitivity y. destruct H as [n [e He H]]. change (-(CRinv_pos (exist _ _ He) (- Cauchy_IRasCR (Build_CauchySeq Q_as_COrdField x Hx)))==y)%CR. unfold y. rewrite <- Cauchy_IR_opp_as_CR_opp. apply CRopp_wd. set (X := (Cauchy_IRasCR (f_rcpcl (F:=Cauchy_IR) [--](x':Cauchy_IR) (@inr (R_lt Q_as_COrdField [--](x':Cauchy_IR) ([0]:Cauchy_IR)) ([0][<][--](x':Cauchy_IR)) H')))%CR). rewrite -> Cauchy_IR_opp_as_CR_opp. eapply Cauchy_IR_inv_as_CRinv_pos. intros i Hi. autorewrite with QposElim. simpl. stepr (0 - x i)%Q; [| simpl; ring]. eapply H. apply Hi. unfold y. apply Cauchy_IRasCR_wd. eapply mult_cancel_lft. left. apply H. stepr ([1]:Cauchy_IR). eapply eq_transitive. apply cring_inv_mult_lft. apply eq_symmetric. eapply eq_transitive;[|apply cring_inv_mult_rht]. apply eq_symmetric. apply x_div_x. apply eq_symmetric. apply x_div_x. destruct H as [n [e He H]]. eapply Cauchy_IR_inv_as_CRinv_pos. intros i Hi. autorewrite with QposElim. simpl in *. stepr (x i- 0)%Q; [| simpl; ring]. apply H. apply Hi. 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