proposition: Lemma applyXsum : forall {X : Set} {R : ConstructiveReals} (fn : nat -> @PartialFunction R X) (n : nat) (x : X) (xD : Domain (Xsum fn n) x) (xn : forall n:nat, Domain (fn n) x), partialApply (Xsum fn n) x xD == CRsum (fun k:nat => partialApply (fn k) x (xn k)) n.
proof: Proof. induction n. - intros x xD xn. simpl. apply DomainProp. - intros x xD xn. simpl. rewrite <- (IHn x (fst xD)). clear IHn. destruct xD. apply CRplus_morph. reflexivity. apply DomainProp. Qed.
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete