proposition: Lemma moda0_exp_compat : forall (a : Z) (n : nat), n > 0 -> Mod a 0 n -> forall m : nat, m > 0 -> Mod (Exp a m) 0 n.
proof: Proof. intros a n. case n. intro. elim (lt_irrefl 0). assumption. intro. intro. intro. intro. case m. intro. elim (lt_irrefl 0). assumption. intro m0. intros. elim H0. intros. rewrite H2. split with (x * Exp (Z_of_nat (S n0) * x) m0)%Z. rewrite Zmult_assoc. simpl in |- *. reflexivity. Qed.
imports: ZArith lemmas natZ exp divides