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