proposition: Lemma FSum_FSum0' : forall P f m n, (forall i, included P (Dom (f i))) -> Feq P (FSum m n f) (FSum0 (S n) f{-}FSum0 m f).
proof: Proof. intros P f m n H. apply eq_imp_Feq. red in |- *; intros; intro; apply (H n0); auto. apply included_FMinus; red in |- *; intros; intro; apply (H n0); auto. intros. apply eq_transitive_unfolded with (Part _ _ (ProjIR1 Hx') [-]FSum0 m f _ (ProjIR2 Hx')). apply FSum_FSum0. simpl in |- *; rational. Qed.
imports: CoRN.reals.CSumsReals CoRN.ftc.PartFunEquality