proposition: Lemma XnegPartNonNeg : forall {R : ConstructiveReals} {X : Set} (f : @PartialFunction R X), nonNegFunc (XnegPart f).
proof: Proof. intros. intros x xdf. destruct xdf. rewrite (DomainProp (XnegPart f) x _ (pair d d)). rewrite (applyXnegPart f x d). apply CRmax_l. Qed.
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete