proposition: Lemma mod_exp_compat : forall (a b : Z) (n : nat), Mod a b n -> forall m : nat, Mod (Exp a m) (Exp b m) n.
proof: Proof. simple induction m. simpl in |- *. apply mod_refl. intros m1 IHm. simpl in |- *. apply mod_mult_compat. assumption. assumption. Qed.
imports: ZArith lemmas natZ exp divides