proposition: Lemma Nfinite_prod_div : forall n f k p, k <= n -> (p | f k) -> (p | Nfinite_prod_0_n n f).
proof: Proof. induction n. intros. inversion H. rewrite H1 in * |- *. simpl. auto. intros. apply le_le_S_eq in H. destruct H. apply le_S_n in H. simpl. apply Ndiv_mult_compat. apply IHn with k. auto. auto. simpl. rewrite Nat.mul_comm. apply Ndiv_mult_compat. rewrite <- H. auto. Qed.
imports: Arith Compare Nk_ind Npow Ndiv