proposition: Lemma fun_seq_part_sum_n : forall f (H' : forall n, Continuous_I Hab (f n)) m n, 0 < n -> m <= n -> Feq I (fun_seq_part_sum f n{-}fun_seq_part_sum f m) (FSum m (pred n) f).
proof: Proof. intros. unfold fun_seq_part_sum in |- *. apply eq_imp_Feq. unfold I in |- *; apply contin_imp_inc; Contin. unfold I in |- *; apply contin_imp_inc; Contin. intros; simpl in |- *. unfold Sum, Sum1 in |- *. rewrite <- (Nat.lt_succ_pred 0 n); auto. apply cg_minus_wd; apply Sum0_wd; intros; rational. Qed.
imports: CoRN.ftc.FunctSequence CoRN.reals.Series