proposition: Theorem pocklington : forall (n q m : nat) (a : Z) (qlist : natlist), n > 1 -> n = S (q * m) -> q = product qlist -> allPrime qlist -> Mod (Exp a (pred n)) 1 n -> allLinCombMod a n m qlist -> n <= q * q -> Prime n.
proof: Proof. intros. apply primepropdiv. assumption. intro p. intros. elim H6. intros. elim H7. intro pdn. intros. unfold gt in |- *. apply le_lt_trans with (pred p * pred p). apply le_trans with (q * q). assumption. cut (q <= pred p). intros. apply le_le_mult. assumption. assumption. apply order_le_predp with (Exp a m). assumption. cut (Mod (Exp (Exp a m) q) 1 p). intros. elim (order_ex (Exp a m) p). intro r. intros. elim H12. intros. elim H14. intros. elim H16. intros. elim (le_lt_or_eq r q). intro. cut (Divides r q). intros. elim (techlemma3 qlist r q). intro qi. intros. elim H21. intros. elim H23. intro rdm. intros. elim (allLinCombMod_ok a n m qlist). intros AH1 AH2. elim (AH1 H4 qi H22). intro alpha. intros. elim H25. intro beta. intros. elim (mod_0not1 p). assumption. apply mod_trans with ((1 - 1) * alpha + Z_of_nat n * beta)%Z. rewrite H10. simpl in |- *. rewrite Znat.inj_mult. rewrite Zmult_assoc_reverse. apply mod_sym. apply mod_nx_0_n. apply mod_trans with ((Exp a (m * multDrop qi qlist) - 1) * alpha + Z_of_nat n * beta)%Z. apply mod_plus_compat. apply mod_mult_compat. apply mod_minus_compat. rewrite H24. rewrite mult_assoc. apply mod_sym. rewrite exp_mult. apply mod_exp1. rewrite exp_mult. assumption. apply mod_refl. apply mod_refl. apply mod_refl. apply mod_sym. apply modpq_modp with pdn. rewrite <- H10. assumption. assumption. assumption. assumption. assumption. assumption. apply (order_div (Exp a m) r p H14 q). apply lt_trans with r. assumption. assumption. assumption. intro. rewrite <- H19. assumption. apply H18. elim (le_lt_or_eq 0 q). intro. assumption. intro. rewrite <- H19 in H5. simpl in H5. elim (le_not_lt n 0). assumption. apply lt_trans with 1. apply lt_O_Sn. assumption. apply le_O_n. assumption. assumption. apply mod_not_exp_0. assumption. intro. elim (mod_0not1 p). assumption. apply mod_trans with (Exp a (pred n)). apply mod_sym. apply moda0_exp_compat. unfold gt in |- *. apply lt_trans with 1. apply lt_O_Sn. assumption. assumption. apply gt_pred. assumption. rewrite H0. simpl in |- *. rewrite mult_comm. rewrite exp_mult. assumption. rewrite H0 in H3. simpl in H3. rewrite <- H0 in H3. apply modpq_modp with pdn. rewrite <- H10. rewrite <- exp_mult. rewrite mult_comm. assumption. apply lt_multpred_pp. assumption. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo gcd modprime order