proposition: Lemma sum_assoc : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (n p : nat), CRsum u (S n + p) == CRsum u n + CRsum (fun k => u (S n + k)%nat) p.
proof: Proof. induction p. - simpl. rewrite Nat.add_0_r. reflexivity. - simpl. rewrite (Radd_assoc (CRisRing R)). apply CRplus_morph. + rewrite Nat.add_succ_r. rewrite (CRsum_eq (fun k : nat => u (S (n + k))) (fun k : nat => u (S n + k)%nat)). * rewrite <- IHp. reflexivity. * intros. reflexivity. + reflexivity. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits