proposition: Theorem Zpocklington : forall (n q m a : Z) (qlist : Zlist), (n > 1)%Z -> (0 <= q)%Z -> (0 <= m)%Z -> n = (q * m + 1)%Z -> q = zproduct qlist -> allZPrime qlist -> ZMod (ZExp a (n - 1)) 1 n -> ZallLinCombMod a n m n qlist -> (n <= q * q)%Z -> ZPrime n.
proof: Proof. intros. cut (0 <= n)%Z. intros. rewrite <- (inj_abs_pos n). apply primezprime. apply (pocklington (Z.abs_nat n) (Z.abs_nat q) (Z.abs_nat m) a (map _ _ Z.abs_nat qlist)). change (Z.abs_nat n > Z.abs_nat 1) in |- *. apply gtzgt. assumption. unfold Z.le in |- *. simpl in |- *. discriminate. assumption. rewrite H2. rewrite abs_plus_pos. rewrite abs_mult. rewrite plus_comm. simpl in |- *. reflexivity. apply isnat_mult. assumption. assumption. unfold Z.le in |- *. simpl in |- *. discriminate. rewrite H3. apply zproductproduct. apply allzprimeallprime. assumption. apply mod_trans with (ZExp a (n - 1)). rewrite <- inj_zexp. rewrite abs_pred_pos. rewrite inj_abs_pos. apply mod_refl. apply Z.le_ge. unfold Zminus in |- *. simpl in |- *. change (0 <= 0 + n + -1)%Z in |- *. rewrite (Zplus_assoc_reverse 0). rewrite Zplus_comm. apply (Zlt_left 0 n). apply Z.lt_trans with 1%Z. unfold Z.lt in |- *. simpl in |- *. reflexivity. apply Z.gt_lt. assumption. apply Z.lt_trans with 1%Z. unfold Z.lt in |- *. simpl in |- *. reflexivity. apply Z.gt_lt. assumption. apply zmodmod. assumption. apply alllincombzalllincomb. assumption. assumption. apply allzprimeallpos. assumption. assumption. rewrite <- abs_mult. apply lezle. assumption. apply isnat_mult. assumption. assumption. assumption. apply Z.le_ge. assumption. apply Z.le_trans with 1%Z. unfold Z.le in |- *. simpl in |- *. discriminate. apply Zlt_le_weak. apply Z.gt_lt. assumption. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo gcd modprime order