proposition: Theorem PocklingtonCorollary2: forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 -> (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) -> forall n, 0 <= n -> (n | N) -> n mod F1 = 1.
proof: Proof. intros N F1 R1 H1 H2 H3 H4 n H5; pattern n; apply prime_induction; auto. assert (HN: 1 < N). cut (0 < N - 1). auto with zarith. rewrite H3. apply Z.lt_le_trans with (1* R1); auto with zarith. intros (u, Hu); contradict HN; subst; rewrite Zmult_0_r; auto with zarith. intro H6; rewrite Zmod_small; auto with zarith. intros p q Hp Hp1 Hp2; rewrite Zmult_mod; auto with zarith. rewrite Pocklington with (n := p) (R1 := R1) (4 := H4); auto. rewrite Hp1. rewrite Zmult_1_r; rewrite Zmod_small; auto with zarith. apply Z.divide_trans with (2 := Hp2); apply Zdivide_factor_l. apply Z.divide_trans with (2 := Hp2); apply Zdivide_factor_r; auto. Qed.
imports: ZArith Znumtheory Tactic ZCAux Zp FGroup EGroup Euler