proposition: Theorem prime_div_factorial_le : forall n p : nat, prime p -> divides p (factorial n) -> p <= n.
proof: Proof. intros n p H; elim n; auto. intros (x, H1); Contradict H; auto. replace p with 1; auto with arith. generalize H1; case x; case p; simpl in |- *; auto; try (intros; discriminate). intros n1 H2; rewrite H2; auto. intros n1 n2; case n2; simpl in |- *; repeat (rewrite <- plus_n_Sm || rewrite <- plus_n_O; simpl in |- *); auto with arith. intros n3; repeat rewrite <- plus_n_Sm; intros; discriminate. intros n0 H0 H1; case (L_Euclides2 p (S n0) (factorial n0)); auto with arith. intros H2; apply divides_le; auto. Qed.
imports: Coq(ArithRing Wf_nat Lia)