proposition: Lemma Xsum_assoc : forall {X : Set} {R : ConstructiveReals} (u : nat -> @PartialFunction R X) (n p : nat) (x : X) (xd : Domain (Xsum u (S n + p)) x) (y : Domain (Xsum u n) x) (z : Domain (Xsum (fun k => u (S n + k)%nat) p) x), partialApply (Xsum u (S n + p)) x xd == partialApply (Xsum u n) x y + partialApply (Xsum (fun k => u (S n + k)%nat) p) x z.
proof: Proof. induction p. - intros. simpl in z. simpl. destruct xd. remember (n + 0)%nat as sn. rewrite Nat.add_0_r in Heqsn. subst sn. apply CRplus_morph. apply DomainProp. apply DomainProp. - intros. simpl. destruct xd. simpl in z. remember (n + S p)%nat as sn. rewrite Nat.add_succ_r in Heqsn. subst sn. rewrite (IHp x _ y (fst z)). clear IHp. rewrite CRplus_assoc. apply CRplus_morph. reflexivity. destruct z. apply CRplus_morph. reflexivity. apply DomainProp. Qed.
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete