proposition: Lemma mod_not_exp_0 : forall p : nat, Prime p -> forall a : Z, ~ Mod a 0 p -> forall m : nat, ~ Mod (Exp a m) 0 p.
proof: Proof. intros p Hp a Ha. simple induction m. simpl in |- *. intro. elim (mod_0not1 p). elim Hp. intros. assumption. apply mod_sym. assumption. simpl in |- *. intros. intro. elim (mod_mult_0 p a (Exp a n) Hp). assumption. assumption. assumption. Qed.
imports: Arith ZArith Wf_nat lemmas natZ dec list exp divides prime modulo gcd