proposition: Theorem PocklingtonCorollary1: forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 -> N < F1 * F1 -> (forall p, prime p -> (p | F1) -> exists a, 1 < a /\ a^(N - 1) mod N = 1 /\ Z.gcd (a ^ ((N - 1)/ p) - 1) N = 1) -> prime N.
proof: Proof. intros N F1 R1 H H1 H2 H3 H4; case (prime_dec N); intros H5; auto. assert (HN: 1 < N). cut (0 < N - 1). auto with zarith. rewrite H2. apply Z.lt_le_trans with (1* R1); auto with zarith. case Zdivide_div_prime_le_square with (2:= H5); auto with zarith. intros n (Hn, (Hn1, Hn2)). assert (Hn3: 0 <= n). apply Z.le_trans with 2; try apply prime_ge_2; auto with zarith. absurd (n = 1). intros H6; contradict Hn; subst; apply not_prime_1. rewrite <- (Zmod_small n F1); try split; auto. apply Pocklington with (R1 := R1) (4 := H4); auto. apply Zlt_square_mult_inv; auto with zarith. Qed.
imports: ZArith Znumtheory Tactic ZCAux Zp FGroup EGroup Euler