proposition: Lemma cond_pos_sum : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (n : nat), (forall k, 0 <= un k) -> 0 <= CRsum un n.
proof: Proof. induction n. - intros. apply H. - intros. simpl. rewrite <- CRplus_0_r. apply CRplus_le_compat. + apply IHn, H. + apply H. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits