proposition: Lemma FSum_S : forall P f m n, (forall i, included P (Dom (f i))) -> Feq P (FSum m n f{+}f (S n)) (FSum m (S n) f).
proof: Proof. intros P f m n H. apply eq_imp_Feq. apply included_FPlus; auto. simpl in |- *. red in |- *; intros; apply (H n0); auto. simpl in |- *. red in |- *; intros; apply (H n0); auto. intros; simpl in |- *; apply eq_symmetric_unfolded. eapply eq_transitive_unfolded. apply Sum_last. algebra. Qed.
imports: CoRN.reals.CSumsReals CoRN.ftc.PartFunEquality