proposition: Lemma times_mod_spec : forall x y n, Z_of_N (times_mod x y n) = (x * y) mod n.
proof: Proof. intros; destruct x; mauto. destruct y;simpl; mauto. Qed.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod