proposition: Lemma Nfinite_sum_split_lower : forall n f, Nfinite_sum_0_n (S n) f = f 0 + Nfinite_sum_0_n n (fun k => f (S k)).
proof: Proof. induction n. compute. auto with arith. intros. unfold Nfinite_sum_0_n. fold Nfinite_sum_0_n. unfold Nfinite_sum_0_n in IHn. fold Nfinite_sum_0_n in IHn. rewrite IHn. rewrite Nat.add_assoc. rewrite Nat.add_assoc. auto with arith. Qed.
imports: Arith Nk_ind Ndiv