proposition: Lemma applyXplus : forall {R : ConstructiveReals} {X : Set} (f g : @PartialFunction R X) (x : X) (xdf : Domain f x) (xdg : Domain g x), partialApply (Xplus f g) x (pair xdf xdg) == partialApply f x xdf + partialApply g x xdg.
proof: Proof. reflexivity. Qed.
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete