proposition: Lemma Nfinite_sum_subtle_eq_compat : forall n f g, (forall k, k <= n -> f k = g k) -> Nfinite_sum_0_n n f = Nfinite_sum_0_n n g.
proof: Proof. induction n. compute. intros. apply H. trivial. intros. unfold Nfinite_sum_0_n. fold Nfinite_sum_0_n. rewrite (IHn f g). rewrite (H (S n)). reflexivity. trivial. intros. apply H. auto with arith. Qed.
imports: Arith Nk_ind Ndiv