proposition: Lemma seq_part_sum_n : forall m n, 0 < n -> m <= n -> seq_part_sum n[-]seq_part_sum m [=] Sum m (pred n) x.
proof: Proof. intros. elim (le_lt_eq_dec _ _ H0); intro. unfold seq_part_sum in |- *. unfold Sum, Sum1 in |- *. rewrite Nat.lt_succ_pred with 0 n; auto. algebra. rewrite b. astepl ZeroR. apply eq_symmetric_unfolded; apply Sum_empty. assumption. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)