fact: Definition Xmin {R : ConstructiveReals} {X : Set} (f g : @PartialFunction R X) : PartialFunction X := Xminus g (XnegPart (Xminus f g)).
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete