proposition: Theorem prime_dirac_divides_binomial : forall n m p : nat, n < p -> m < p -> p <= n + m -> divides (prime_dirac p) (binomial (n + m) n).
proof: Proof. intros n m p H H0 H1. unfold prime_dirac in |- *; generalize (primeb_correct p); case (primeb p); auto. intros H2. apply L_Euclides1 with (a := factorial m); auto with arith. apply L_Euclides1 with (a := factorial n); auto with arith. rewrite Nat.mul_assoc. rewrite (fun x y z => Nat.mul_comm (x * y) z). rewrite binomial_fact. generalize H1; elim m; simpl in |- *; auto with arith. rewrite <- plus_n_O; intros H3; Contradict H; auto with arith. intros m1; repeat rewrite <- plus_n_Sm. intros H3 H4; inversion H4; auto. exists (factorial (n + m1)); rewrite Nat.mul_comm; simpl in |- *; auto. apply divides_trans with (1 := H3 H6). exists (S (n + m1)); auto. red in |- *; intros H3; contradict H; auto with arith. apply Nat.le_ngt; apply prime_div_factorial_le; auto. red in |- *; intros H3; contradict H0; auto with arith. apply Nat.le_ngt; apply prime_div_factorial_le; auto. Qed.
imports: Coq(ArithRing Wf_nat Lia)