proposition: Lemma Cauchy_IRasCauchy_IR : forall x:Cauchy_IR, CRasCauchy_IR (Cauchy_IRasCR x)[=]x.
proof: Proof. intros [x Hx]. eapply Eq_alt_2_2. intros e He. assert (Z:(0<(1#2)*e)%Q). rewrite <- (Qmult_0_r (1#2)). eapply mult_resp_less_lft. exact He. constructor. destruct (Hx _ Z) as [n Hn]. destruct e as [en ed]. destruct en as [|en|en]. inversion He. 2: inversion He. exists (Nat.max n (nat_of_P ed)). intros m Hm. simpl. destruct Hx as [n' Hn']. apply AbsSmall_minus. destruct (le_lt_dec n' m) as [H|H]. eapply AbsSmall_trans;[|apply Hn';assumption]. change (ed < en*(P_of_succ_nat m))%Z. apply Z.lt_le_trans with (P_of_succ_nat m). rewrite <- POS_anti_convert. rewrite Zpos_eq_Z_of_nat_o_nat_of_P. apply inj_lt. apply Nat.lt_succ_r. apply Nat.le_trans with (Nat.max n (nat_of_P ed));auto with *. change (1*P_of_succ_nat m <= en * P_of_succ_nat m)%Z. apply Zmult_lt_0_le_compat_r;auto with *. stepl ((1#2)*(Z.pos en#ed)+(1#2)*(Z.pos en#ed))%Q; [| simpl; ring]. rstepr ((x m[-]x n)[+](x n[-]x n')). assert (Y:n <= m). apply Nat.le_trans with (Nat.max n (nat_of_P ed));auto with *. apply AbsSmall_plus. apply Hn. assumption. apply AbsSmall_minus; 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