proposition: Lemma PosSumMaj : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (a : CRcarrier R) (k : nat), (forall n:nat, 0 <= un n) -> CRsum un k <= a -> un k <= a.
proof: Proof. destruct k. - intros. exact H0. - intros. simpl in H0. rewrite <- (CRplus_0_l (un (S k))). apply (CRle_trans _ (CRsum un k + un (S k))). apply CRplus_le_compat. apply cond_pos_sum. exact H. apply CRle_refl. exact H0. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions