fact: Definition partialFuncLe {R : ConstructiveReals} {X : Set} (f g : @PartialFunction R X) : Prop := forall (x : X) (xdf : Domain f x) (xdg : Domain g x), partialApply f x xdf <= partialApply g x xdg.
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete