proposition: Lemma applyXminus : forall {R : ConstructiveReals} {X : Set} (f g : @PartialFunction R X) (x : X) (xdf : Domain f x) (xdg : Domain g x), partialApply (Xminus f g) x (pair xdf xdg) == partialApply f x xdf - partialApply g x xdg.
proof: Proof. intros. apply CRplus_morph. reflexivity. rewrite applyXscale. rewrite <- CRopp_mult_distr_l. rewrite CRmult_1_l. reflexivity. Qed.
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete