proposition: Lemma mod_exp1 : forall (a : Z) (n : nat), Mod a 1 n -> forall m : nat, Mod (Exp a m) 1 n.
proof: Proof. intros a n H. simple induction m. simpl in |- *. apply mod_refl. intros m1 IH. simpl in |- *. replace 1%Z with (1 * 1)%Z. apply mod_mult_compat. assumption. apply IH. simpl in |- *. reflexivity. Qed.
imports: ZArith lemmas natZ exp divides