proposition: Lemma zmod_exp_compat : forall a b n : Z, ZMod a b n -> forall m : Z, ZMod (ZExp a m) (ZExp b m) n.
proof: Proof. intros. apply absmodzmod. rewrite expzexp. rewrite expzexp. apply mod_exp_compat. apply zmodmod. assumption. Qed.
imports: ZArith lemmas natZ exp divides