proposition: Lemma nonNegSumFunc {R : ConstructiveReals} {X : Set} (fn : nat -> @PartialFunction R X) : (forall n:nat, nonNegFunc (fn n)) -> (forall n:nat, nonNegFunc (Xsum fn n)).
proof: Proof. intros. induction n. - intros x. simpl. apply H. - intros x. simpl. apply nonNegFuncPlus. assumption. apply H. Qed.
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete