proposition: Lemma zmodpq_modp : forall a b p q : Z, ZMod a b (p * q) -> ZMod a b p.
proof: Proof. unfold ZMod in |- *. intros. elim H. intros. split with (q * x)%Z. rewrite Zmult_assoc. assumption. Qed.
imports: ZArith lemmas natZ exp divides