proposition: Lemma Pmod_Zmod : forall a b, Z_of_N (a mod b)%P = a mod b.
proof: Proof. intros a b; rewrite Pmod_div_eucl. assert (b>0). mauto. unfold Z.modulo; assert (H1 := Z_div_mod a b H). destruct (Z.div_eucl a b) as (q2, r2). assert (H2 := div_eucl_spec a b). assert (Z_of_N (fst (a / b)%P) = q2 /\ Z_of_N (snd (a/b)%P) = r2). destruct H1;destruct H2. apply mod_unique with b. 2: mauto. split. 2: mauto. unfold Z.le;destruct (snd (a / b)%P);intro;discriminate. rewrite <- H0;symmetry;rewrite Zmult_comm;trivial. destruct H0;auto. Qed.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod