proposition: Lemma CRmorph_cv : forall {R1 R2 : ConstructiveReals} (f : @ConstructiveRealsMorphism R1 R2) (un : nat -> CRcarrier R1) (l : CRcarrier R1), CR_cv R1 un l -> CR_cv R2 (fun n => CRmorph f (un n)) (CRmorph f l).
proof: Proof. intros. intro p. specialize (H p) as [n H]. exists n. intros. specialize (H i H0). unfold CRminus. rewrite <- CRmorph_opp, <- CRmorph_plus, CRmorph_abs. rewrite <- (CRmorph_rat f (1#p)). apply CRmorph_le. exact H. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveLimits ConstructiveAbs