proposition: Lemma Nfinite_sum_eq_compat : forall n f g, (forall k, f k = g k) -> Nfinite_sum_0_n n f = Nfinite_sum_0_n n g.
proof: Proof. intros. apply Nfinite_sum_subtle_eq_compat. intros. apply H. Qed.
imports: Arith Nk_ind Ndiv