proposition: Lemma CRasCauchy_IR_raw_is_Cauchy : forall (x:CR), Cauchy_prop (R:=Q_as_COrdField) (CRasCauchy_IR_raw x).
proof: Proof. intros x e He. destruct e as [en ed]. destruct en as [|en|en]. inversion He. 2: inversion He. unfold CRasCauchy_IR_raw. exists (pred (nat_of_P (2*ed))). rewrite <- anti_convert_pred_convert. intros m Hm. change (ball (en#ed) (approximate x (Qpos2QposInf (1 # P_of_succ_nat m))) (approximate x (Qpos2QposInf (1#(2*ed))))). eapply ball_weak_le ;[|apply regFun_prf]. simpl. apply Qle_trans with (((1 # P_of_succ_nat (pred (nat_of_P (2*ed)))) + (1 # 2 * ed)))%Q. eapply plus_resp_leEq. change (P_of_succ_nat (pred (nat_of_P (2*ed))) <= P_of_succ_nat m)%Z. rewrite <-!POS_anti_convert. apply inj_le. lia. rewrite <- anti_convert_pred_convert. stepl ((2#1)*(1#(2*ed)))%Q; [|simpl; ring]. change ((2#1)*((1/2)*(1/ed)) <= en#ed)%Q. ring_simplify. change ((2#2)*(1/ed)<=en#ed)%Q. setoid_replace (2#2)%Q with 1%Q by constructor. ring_simplify. 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