proposition: Lemma modzmod : forall (a b : Z) (n : nat), Mod a b n -> ZMod a b (Z_of_nat n).
proof: Proof. unfold Mod, ZMod in |- *. intros. elim H. intros. rewrite H0. split with x. reflexivity. Qed.
imports: ZArith lemmas natZ exp divides