proposition: Lemma CR_cv_extens : forall {R : ConstructiveReals} (xn yn : nat -> CRcarrier R) (l : CRcarrier R), (forall n:nat, xn n == yn n) -> CR_cv R xn l -> CR_cv R yn l.
proof: Proof. intros. intro p. specialize (H0 p) as [n nmaj]. exists n. intros. specialize (nmaj i H0). apply (CRle_trans _ (CRabs R (CRminus R (xn i) l))). 2: exact nmaj. rewrite <- CRabs_def. split. - apply (CRle_trans _ (CRminus R (xn i) l)). + apply CRplus_le_compat_r. specialize (H i) as [H _]. exact H. + pose proof (CRabs_def R (CRminus R (xn i) l) (CRabs R (CRminus R (xn i) l))) as [_ H1]. apply H1. apply CRle_refl. - apply (CRle_trans _ (CRopp R (CRminus R (xn i) l))). + intro abs. apply CRopp_lt_cancel, CRplus_lt_reg_r in abs. specialize (H i) as [_ H]. contradiction. + pose proof (CRabs_def R (CRminus R (xn i) l) (CRabs R (CRminus R (xn i) l))) as [_ H1]. apply H1. apply CRle_refl. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs