proposition: Lemma Xsum_assocMinus : forall {X : Set} {R : ConstructiveReals} (u : nat -> @PartialFunction R X) (n p : nat) (x : X) (px : Domain (Xminus (Xsum u (S n + p)) (Xsum u n)) x) (pxD : Domain (Xsum (fun k => u (S n + k)%nat) p) x), partialApply (Xminus (Xsum u (S n + p)) (Xsum u n)) x px == partialApply (Xsum (fun k => u (S n + k)%nat) p) x pxD.
proof: Proof. induction p. - intros. simpl in px, pxD. transitivity (partialApply (u (S n + 0)%nat) x pxD). 2: reflexivity. simpl (S n + 0)%nat. remember (n + 0)%nat. rewrite Nat.add_0_r in Heqn0. subst n0. destruct px. rewrite applyXminus. rewrite <- (CRplus_0_r (partialApply (u (S n)) x pxD)). unfold CRminus. destruct p. simpl. rewrite (CRplus_comm (partialApply (Xsum u n) x d0)). rewrite CRplus_assoc. apply CRplus_morph. apply DomainProp. rewrite (DomainProp _ _ d0 d). rewrite CRplus_opp_r. reflexivity. - intros. destruct px. rewrite (applyXminus (Xsum u (S n + S p)) (Xsum u n) x d d0). simpl. simpl in d. destruct d, pxD. simpl in d3. remember (n + S p)%nat. rewrite Nat.add_succ_r in Heqn0. subst n0. specialize (IHp x (pair d d0) d2). rewrite <- IHp. rewrite (applyXminus (Xsum u (S n + p)) (Xsum u n)). unfold CRminus. rewrite (DomainProp _ x d1 d3). do 2 rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite CRplus_comm. reflexivity. Qed.
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete