proposition: Lemma sumLastElem : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (n : nat), (forall k:nat, lt k n -> un k == 0) -> CRsum un n == un n.
proof: Proof. intros. destruct n. - reflexivity. - simpl. rewrite <- (CRplus_0_l (un (S n))). apply CRplus_morph. rewrite (CRsum_eq _ (fun n => 0)). rewrite sum_const. rewrite CRmult_0_l. reflexivity. intros. apply H. apply le_n_S. assumption. apply CRplus_0_l. Qed.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits