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