proposition: Lemma applyXmin : forall {X : Set} {R : ConstructiveReals} (f g : @PartialFunction R X) (x : X) (xdf : Domain f x) (xdg : Domain g x) (xdp : Domain (Xmin f g) x), partialApply (Xmin f g) x xdp == CRmin (partialApply f x xdf) (partialApply g x xdg).
proof: Proof. intros. unfold Xmin. destruct xdp. rewrite (applyXminus g (XnegPart (Xminus f g))). assert (Domain (Xminus f g) x). { destruct f,g; split. exact xdf. exact xdg. } simpl in d0. unfold CRminus. rewrite (DomainProp (XnegPart (Xminus f g)) x _ (fst d0, fst d0)), applyXnegPartMin. destruct d0,p. unfold fst. rewrite (applyXminus f g). destruct f, g; simpl. rewrite CRopp_involutive. unfold CRminus. rewrite (DomainProp1 x d1 d), (DomainProp1 x xdg d), (DomainProp0 x _ xdf). rewrite CRmin_plus, CRplus_0_r, (CRplus_comm (partialApply0 x xdf)). rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. apply CRmin_sym. Qed.
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete