proposition: Lemma sum_opp : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (n : nat), CRsum (fun k => - un k) n == - CRsum un n.
proof: Proof. induction n. - reflexivity. - simpl. rewrite IHn. rewrite CRopp_plus_distr. reflexivity. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits