proposition: Lemma sum_truncate_above : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (N n : nat), le N n -> CRsum (fun n0 : nat => if le_dec n0 N then u n0 else 0) n == CRsum u N.
proof: Proof. intros. destruct (Nat.eq_dec N n). - subst N. apply CRsum_eq. intros. destruct (le_dec i n). reflexivity. contradiction. - destruct (Nat.le_exists_sub (S N) n) as [p [H0 _]]. + pose proof (Nat.lt_ge_cases N n) as [H0|H1]. apply H0. exfalso. exact (n0 (Nat.le_antisymm N n H H1)). + subst n. rewrite Nat.add_comm. rewrite sum_assoc. assert (CRsum (fun k : nat => if le_dec (S N + k) N then u (S N + k)%nat else 0) p == 0). { rewrite <- (CRsum_eq (fun k => 0)). rewrite sum_const. apply CRmult_0_l. intros. destruct (le_dec (S N + i)). exfalso. assert (S N <= N)%nat. apply (Nat.le_trans (S N) (S N + i)). apply Nat.le_add_r. assumption. exact (Nat.nle_succ_diag_l N H1). reflexivity. } rewrite H0. rewrite CRplus_0_r. rewrite (CRsum_eq u (fun n1 : nat => if le_dec n1 N then u n1 else 0)). reflexivity. intros. destruct (le_dec i N). reflexivity. contradiction. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase