proposition: Lemma CR_cv_proper : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (a b : CRcarrier R), CR_cv R un a -> a == b -> CR_cv R un b.
proof: Proof. intros. intro p. specialize (H p) as [n H]. exists n. intros. unfold CRminus. rewrite <- H0. apply H, H1. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs