proposition: Theorem prime_power_div: forall p q i, prime p -> 0 <= q -> 0 <= i -> (q | p ^ i) -> exists j, 0 <= j <= i /\ q = p ^ j.
proof: Proof. intros p q i Hp Hq Hi H. assert (Hp1: 0 < p). apply Z.lt_le_trans with 2; try apply prime_ge_2; auto with zarith. pattern q; apply prime_div_induction with (p ^ i); auto with zarith. exists 0; rewrite Zpower_0_r; auto with zarith. intros p1 i1 Hp2 Hi1 H1. case Zle_lt_or_eq with (1 := Hi1); clear Hi1; intros Hi1; subst. assert (Heq: p1 = p). apply prime_div_Zpower_prime with i; auto. apply Z.divide_trans with (2 := H1). apply Zpower_divide; auto with zarith. exists i1; split; auto; try split; auto with zarith. case (Zle_or_lt i1 i); auto; intros H2. absurd (p1 ^ i1 <= p ^ i). apply Zlt_not_le; rewrite Heq; apply Zpower_lt_monotone; auto with zarith. apply Z.lt_le_trans with 2; try apply prime_ge_2; auto with zarith. apply Zdivide_le; auto with zarith. rewrite Heq; auto. exists 0; repeat rewrite Zpower_exp_0; auto with zarith. intros p1 q1 Hpq (j1,((Hj1, Hj2), Hj3)) (j2, ((Hj4, Hj5), Hj6)). case Zle_lt_or_eq with (1 := Hj1); clear Hj1; intros Hj1; subst. case Zle_lt_or_eq with (1 := Hj4); clear Hj4; intros Hj4; subst. inversion Hpq as [ H0 H1 H2]. absurd (p | 1). intros H3; absurd (1 < p). apply Zle_not_lt; apply Zdivide_le; auto with zarith. apply Z.lt_le_trans with 2; try apply prime_ge_2; auto with zarith. apply H2; apply Zpower_divide; auto with zarith. exists j1; rewrite Zpower_0_r; auto with zarith. exists j2; rewrite Zpower_0_r; auto with zarith. Qed.
imports: ZCAux List Root UList IGroup EGroup FGroup