proposition: Lemma IR_Cauchy_prop_as_CR : forall (x:CauchySeq IR), (@Cauchy_prop CRasCOrdField (fun n => (IRasCR (x n)))).
proof: Proof. intros x. assert (X:=map_pres_Lim _ _ (iso_map_rht CRasCReals IR CRIR_iso) _ _ (Cauchy_complete x)). intros e He. destruct (X _ (pos_div_two _ _ He)) as [n Hn]. exists n. intros m Hm. assert (A:=Hn m Hm). assert (B:=Hn n (le_n n)). set (a:=(IRasCR (x m))) in *. set (b:=IRasCR (Lim (IR:=IR) x)) in *. set (c:=IRasCR (x n)) in *. setoid_replace (@cg_minus CRasCGroup a c) with (a-b+(b-c))%CR by (unfold cg_minus; simpl; ring). apply (AbsSmall_eps_div_two CRasCOrdField e (a-b)%CR (b-c)%CR). assumption. apply (AbsSmall_minus CRasCOrdField (e [/]TwoNZ) c b). assumption. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.CauchySeq CoRN.reals.iso_CReals CoRN.reals.R_morphism CoRN.reals.fast.CRArith CoRN.model.reals.CRreal CoRN.tactics.CornTac