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