proposition: Lemma Npred_mod_spec : forall p n, Z_of_N p < Zpos n -> 1 < Zpos n -> Z_of_N (Npred_mod p n) = (p - 1) mod n.
proof: Proof. destruct p;intros;simpl. rewrite <- Ppred_Zminus; auto. apply Zmod_unique with (q := -1); mauto. assert (H1 := pos_eq_1_spec p);destruct (p?=1)%P. rewrite H1; mauto. unfold Z_of_N;rewrite <- Ppred_Zminus; auto. simpl in H;symmetry; apply (lt_Zmod (p-1) n). assert (1 < p); auto with zarith. Qed.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod