proposition: Lemma lt_Zmod : forall p n, 0 <= p < n -> p mod n = p.
proof: Proof. intros a b H. assert ( 0 <= a mod b < b). apply Z_mod_lt; mauto. destruct (mod_unique b (a/b) (a mod b) 0 a H0 H); mauto. rewrite <- Z_div_mod_eq_full; mauto. Qed.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod