proposition: Lemma applyXabs : forall {R : ConstructiveReals} {X : Set} (f : PartialFunction X) (x : X) (xD : Domain f x), partialApply (Xabs f) x xD = CRabs R (partialApply f x xD).
proof: Proof. reflexivity. Qed.
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete