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