proposition: Theorem Nbinomial_div : forall p k, 0 < k < p -> Nprime p -> (p | Nbinomial p k).
proof: Proof. intros. assert((p|(fact k)*Nbinomial p k)). rewrite Nbinomial_factorial. apply Nfinite_prod_div with 0. destruct H. destruct k. inversion H. simpl. auto with arith. rewrite Nat.sub_0_r. apply Ndiv_n_n. destruct H. destruct k. inversion H. auto with arith. destruct H. auto with arith. apply Ngauss with (fact k). auto. clear H1. generalize k H. clear H k. induction k. intros. inversion H. inversion H1. intros. destruct H. unfold fact. fold fact. destruct k. simpl. apply Nrel_prime_1. apply Nrel_prime_mult_compat. apply Nrel_prime_sym. apply Nprime_le_rel_prime. auto. split. auto with arith. auto. apply IHk. split. auto with arith. auto with arith. Qed.
imports: Arith Compare Nfinite_prod Ndiv