proposition: Lemma intTelescopicAbs : forall {IS : IntegrationSpace} (fn : nat -> PartialFunction (X (ElemFunc IS))) (fnL : forall n:nat, L (ElemFunc IS) (fn n)) (n : nat), CRsum (fun n : nat => I IS (telescopicOp (X (ElemFunc IS)) fn (CRabs _) (CRabs_morph_prop _) n) (telescopicOpL fn fnL (CRabs _) (CRabs_morph_prop _) (fun f => LabsStable (ElemFunc IS) f) n)) n == Iabs (Xsum fn n) (LsumStable fn fnL n).
proof: Proof. induction n. - reflexivity. - unfold CRsum. rewrite IHn. clear IHn. unfold telescopicOp, telescopicOpL, Xminus. rewrite Iadditive. rewrite Ihomogeneous. rewrite <- (CRopp_mult_distr_l 1), CRmult_1_l. unfold Iabs, Xabs. rewrite <- CRplus_assoc, CRplus_comm, <- CRplus_assoc. rewrite CRplus_opp_l, CRplus_0_l. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase