proposition: Lemma sum_plus : forall {R : ConstructiveReals} (u v : nat -> CRcarrier R) (n : nat), CRsum (fun n0 : nat => u n0 + v n0) n == CRsum u n + CRsum v n.
proof: Proof. induction n. - reflexivity. - simpl. rewrite IHn. do 2 rewrite CRplus_assoc. apply CRplus_morph. + reflexivity. + rewrite CRplus_comm, CRplus_assoc. apply CRplus_morph. * reflexivity. * apply CRplus_comm. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits