proposition: Lemma applyXposPart : forall {X : Set} {R : ConstructiveReals} (f : @PartialFunction R X) (x : X) (xD : Domain f x), partialApply (XposPart f) x (pair xD xD) == CRmax 0 (partialApply f x xD).
proof: Proof. intros. rewrite CRposPartAbsMax. unfold XposPart. rewrite applyXscale. rewrite CRmult_comm. apply CRmult_morph. 2: reflexivity. destruct f; simpl. reflexivity. Qed.
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete