proposition: Lemma Nfinite_sum_mult_distrib : forall a n f, a * Nfinite_sum_0_n n f = Nfinite_sum_0_n n (fun k => a * f k).
proof: Proof. induction n. compute. reflexivity. intros. unfold Nfinite_sum_0_n. fold Nfinite_sum_0_n. rewrite <- IHn. ring. Qed.
imports: Arith Nk_ind Ndiv