proposition: Lemma CR_cv_const : forall {R : ConstructiveReals} (a : CRcarrier R), CR_cv R (fun n => a) a.
proof: Proof. intros a p. exists O. intros. unfold CRminus. rewrite CRplus_opp_r. rewrite CRabs_right. - apply CR_of_Q_le. discriminate. - apply CRle_refl. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs