proposition: Lemma CR_cauchy_eq : forall {R : ConstructiveReals} (un vn : nat -> CRcarrier R), (forall n:nat, un n == vn n) -> CR_cauchy R un -> CR_cauchy R vn.
proof: Proof. intros. intro p. specialize (H0 p) as [n H0]. exists n. intros. specialize (H0 i j H1 H2). unfold CRminus in H0. rewrite <- CRabs_def. rewrite <- CRabs_def in H0. do 2 rewrite H in H0. exact H0. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs