proposition: Lemma ARtoCR_preserves_cauchy : forall xn : nat → AR, ARcauchy_sequence xn -> CRcauchy_sequence (fun n => cast AR CR (xn n)).
proof: Proof. intros xn xncau p. specialize (xncau p) as [n J]. exists n. intros. apply (J i j H5 H6); clear J. destruct (CRtoAR_preserves_ltT (' (1 # p))%CR (CRabs (' ARplus (xn i) (ARopp (xn j))))) as [c _]. apply (ARltT_wd _ _ (reflexivity _) (' CRabs (' ARplus (xn i) (ARopp (xn j))))). - rewrite <- ARtoCR_preserves_abs. apply CRAR_id. - pose proof (inject_Q_AR_CR (1#p)). symmetry in H8. apply (ARltT_wd _ _ H8 _ _ (reflexivity _)). clear H8. apply c; clear c. apply (CRlt_le_trans _ _ _ H7); clear H7. setoid_replace ((' xn i)%mc - (' xn j)%mc)%CR with (cast AR CR (ARplus (xn i) (ARopp (xn j)))). apply CRle_refl. pose proof (ARtoCR_preserves_plus (xn i) (ARopp (xn j))). rewrite H7. apply ucFun2_wd. reflexivity. pose proof (ARtoCR_preserves_opp (xn j)). rewrite H8. apply Cmap_wd. reflexivity. reflexivity. Qed.
imports: Coq.Reals.Abstract.ConstructiveReals CoRN.reals.faster.ARArith CoRN.reals.faster.ARabs CoRN.metric2.Metric CoRN.metric2.Complete CoRN.metric2.MetricMorphisms CoRN.model.metric2.Qmetric CoRN.model.totalorder.QposMinMax CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs ConstructiveFastReals