proposition: Lemma applyXmax : forall {X : Set} {R : ConstructiveReals} (f g : @PartialFunction R X) (x : X) (xdf : Domain f x) (xdg : Domain g x) (xdp : Domain (Xmax f g) x), partialApply (Xmax f g) x xdp == CRmax (partialApply f x xdf) (partialApply g x xdg).
proof: Proof. intros. unfold Xmax. destruct xdp. rewrite applyXplus. assert (Domain (Xminus f g) x). { destruct f,g; split. exact xdf. exact xdg. } rewrite (DomainProp (XposPart (Xminus f g)) x _ (fst d0, fst d0)), applyXposPart. destruct d0, d0. unfold fst. rewrite (applyXminus f g). destruct f, g; simpl. rewrite (DomainProp1 x d2 d), (DomainProp1 x xdg d), (DomainProp0 x d0 xdf). unfold CRminus. rewrite CRmax_plus, CRplus_0_r, (CRplus_comm (partialApply0 x xdf)). rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. apply CRmax_sym. Qed.
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete