proposition: Lemma CR_cv_nonneg : forall {R : ConstructiveReals} (An:nat -> CRcarrier R) (l:CRcarrier R), CR_cv R An l -> (forall n:nat, 0 <= An n) -> 0 <= l.
proof: Proof. intros. intro abs. destruct (Un_cv_nat_real _ l H (-l)) as [N H1]. - rewrite <- CRopp_0. apply CRopp_gt_lt_contravar. apply abs. - specialize (H1 N (Nat.le_refl N)). pose proof (CRabs_def R (An N - l) (CRabs R (An N - l))) as [_ H2]. apply (CRle_lt_trans _ _ _ (CRle_abs _)) in H1. apply (H0 N). apply (CRplus_lt_reg_r (-l)). rewrite CRplus_0_l. exact H1. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs