proposition: Lemma IR_Sum0_as_CR : forall m x, (IRasCR (Sum0 m x)==@Sum0 CRasCAbGroup m (fun n => IRasCR (x n)))%CR.
proof: Proof. intros m x. induction m. apply IR_Zero_as_CR. simpl in *. set (a:=Sum0 (G:=CRasCAbGroup) m (fun n : nat => IRasCR (x n))) in *. clearbody a. rewrite <- IHm. apply IR_plus_as_CR. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.CauchySeq CoRN.reals.iso_CReals CoRN.reals.R_morphism CoRN.reals.fast.CRArith CoRN.model.reals.CRreal CoRN.tactics.CornTac