proposition: Lemma Nfinite_sum_div_compat : forall n f p, (forall k, k <= n -> (p | f k)) -> (p | Nfinite_sum_0_n n f).
proof: Proof. induction n. intros. simpl. apply H. auto. intros. rewrite Nfinite_sum_split_upper. apply Ndiv_plus_compat. apply IHn. intros. apply H. auto with arith. apply H. auto. Qed.
imports: Arith Nk_ind Ndiv