proposition: Lemma applyXposPartNonNeg : forall {X : Set} {R : ConstructiveReals} (f : @PartialFunction R X), nonNegFunc (XposPart f).
proof: Proof. intros. intros x xdf. unfold XposPart. rewrite applyXscale. rewrite <- (CRmult_0_r (CR_of_Q _ (1#2))). apply CRmult_le_compat_l_half. apply CR_of_Q_pos. reflexivity. destruct f,xdf; simpl. rewrite <- (CRplus_opp_r (partialApply0 x d)). apply CRplus_le_compat_l. setoid_replace (partialApply0 x d0) with (partialApply0 x d). rewrite <- CRabs_opp. apply CRle_abs. apply DomainProp0. Qed.
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete