proposition: Lemma ARcauchy_complete : ∀ xn : nat → AR, ARcauchy_sequence xn → sigT (fun l : AR => ∀ p : positive, {n : nat | ∀ i : nat, (n <= i)%nat → ARltT (inject_Q_AR (1 # p)) (ARabs (ARplus (xn i) (ARopp l))) → False}).
proof: Proof. intros. destruct (CRcauchy_complete _ (ARtoCR_preserves_cauchy xn H5)) as [l J]. exists (cast CR AR l). intro p. specialize (J p) as [n J]. exists n. intros i H6 H7. specialize (J i H6). apply J. unfold ARabs in H7. destruct (CRtoAR_preserves_ltT (' (1 # p))%CR (CRabs (' ARplus (xn i) (ARopp (' l))))) as [_ c]. apply (ARltT_wd _ _ (reflexivity _) _ (' CRabs (' ARplus (xn i) (ARopp ('l))))) in H7. - pose proof (inject_Q_AR_CR (1#p)). apply (ARltT_wd _ _ H8 _ _ (reflexivity _)) in H7. clear H8. apply c in H7; clear c. apply (CRlt_le_trans _ _ _ H7). setoid_replace ((' xn i)%mc - l)%CR with (cast AR CR (ARplus (xn i) (ARopp (' l)))). apply CRle_refl. pose proof (ARtoCR_preserves_plus (xn i) (ARopp ('l))). rewrite H8. apply ucFun2_wd. reflexivity. pose proof (ARtoCR_preserves_opp ('l)). rewrite H9. apply Cmap_wd. reflexivity. symmetry. apply CRAR_id. - rewrite <- ARtoCR_preserves_abs. symmetry. apply CRAR_id. 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