proposition: Lemma pos_sum_more : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (n p : nat), (forall k:nat, 0 <= u k) -> le n p -> CRsum u n <= CRsum u p.
proof: Proof. intros. destruct (Nat.le_exists_sub n p H0). destruct H1. subst p. rewrite Nat.add_comm. destruct x. - rewrite Nat.add_0_r. apply CRle_refl. - rewrite Nat.add_succ_r. replace (S (n + x)) with (S n + x)%nat. + rewrite sum_assoc. rewrite <- CRplus_0_r, CRplus_assoc. apply CRplus_le_compat_l. rewrite CRplus_0_l. apply cond_pos_sum. intros. apply H. + auto. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits