proposition: Lemma Zmult_mod_r : forall (n:positive) a b, (a * (b mod n)) mod n = (a * b) mod n.
proof: Proof. Proof with mauto. intros;rewrite Zmult_mod ... rewrite (Zmult_mod a) ... Qed.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod