proposition: Lemma CR_cv_eq : forall {R : ConstructiveReals} (v u : nat -> CRcarrier R) (s : CRcarrier R), (forall n:nat, u n == v n) -> CR_cv R u s -> CR_cv R v s.
proof: Proof. intros R v u s seq H1 p. specialize (H1 p) as [N H0]. exists N. intros. unfold CRminus. rewrite <- seq. apply H0, H. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs