proposition: Lemma applyXnegPartNonNeg : forall {X : Set} {R : ConstructiveReals} (f : @PartialFunction R X), nonNegFunc (XnegPart f).
proof: Proof. intros. intros y ydf. unfold XnegPart. rewrite applyXscale. rewrite <- (CRmult_0_r (CR_of_Q _ (1#2))). apply CRmult_le_compat_l_half. apply CR_of_Q_pos. reflexivity. destruct ydf; simpl. rewrite <- CRopp_mult_distr_l, CRmult_1_l. rewrite <- (CRplus_opp_r (partialApply f y d0)). apply CRplus_le_compat_r. rewrite (DomainProp f y d0 d). apply CRle_abs. Qed.
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete