proposition: Theorem div_power_prime : forall p w n : nat, prime p -> divides p (power w n) -> divides p w.
proof: Proof. intros p w n; elim n; simpl in |- *; auto. intros H' (q, H'0). generalize H' H'0; case q; case p; simpl in |- *; intros; try discriminate. Contradict H'1; auto with arith. generalize H'2; case n0; simpl in |- *; auto. intros n2 H'3; Contradict H'3; auto with arith. intros n0 H' H'0 H'1. case (divides_dec p (power w n0)); intros H; auto. apply L_Euclides1 with (a := power w n0); auto. rewrite Nat.mul_comm; auto. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)