proposition: Lemma Zpower_0 : forall p : positive, 0^p = 0.
proof: Proof. intros;simpl;destruct p;unfold Zpower_pos;simpl;trivial. generalize (iter_pos Z (Z.mul 0) 1 p). induction p;simpl;trivial. Qed.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod