proposition: Lemma TelescopicSum : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (n : nat), CRsum (fun k => un (S k) - un k) n == un (S n) - (un O).
proof: Proof. induction n. - reflexivity. - simpl. rewrite IHn. rewrite CRplus_comm. unfold CRminus. rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. reflexivity. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal