proposition: Lemma seq_cv_le : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (l a : CRcarrier R), CR_cv R un l -> (forall n:nat, un n <= a) -> l <= a.
proof: Proof. intros. apply (CR_cv_bound_up un a l O). intros. apply H0. apply H. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions