proposition: Lemma Nfinite_sum_plus_compat : forall n f g, Nfinite_sum_0_n n f + Nfinite_sum_0_n n g = Nfinite_sum_0_n n (fun k => f k + g k).
proof: Proof. induction n. compute. reflexivity. intros. unfold Nfinite_sum_0_n. fold Nfinite_sum_0_n. rewrite <- Nat.add_assoc. rewrite <- Nat.add_assoc. assert (g (S n) + Nfinite_sum_0_n n g = Nfinite_sum_0_n n g + g (S n)). auto with arith. rewrite H. clear H. assert (Nfinite_sum_0_n n f + (Nfinite_sum_0_n n g + g (S n)) = Nfinite_sum_0_n n f + Nfinite_sum_0_n n g + g (S n)). auto with arith. rewrite H. clear H. rewrite IHn. auto with arith. Qed.
imports: Arith Nk_ind Ndiv