fact: Definition XmaxConst {R : ConstructiveReals} {X : Set} (f : @PartialFunction R X) (a : CRcarrier R) : PartialFunction X := Xop X f (fun x => CRmax x a) (fun x y Hxy => CRmax_morph _ x y Hxy a a (CReq_refl a)).
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete