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