proposition: Lemma nonNegFuncPlus {R : ConstructiveReals} {X : Set} (f g : @PartialFunction R X) : nonNegFunc f -> nonNegFunc g -> nonNegFunc (Xplus f g).
proof: Proof. intros H H0 x xdf. destruct xdf; simpl. apply (CRle_trans _ (partialApply f x d + 0)). rewrite CRplus_0_r. apply H. apply CRplus_le_compat_l. apply H0. Qed.
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete