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