proposition: Theorem Zdivide_power_2 x p n : 0 <= n -> 0 <= x -> prime p -> (x | p^n) -> exists m, x = p^m.
proof: Proof. intros Hn Hx; revert p n Hn. generalize Hx. pattern x; apply Z_lt_induction; auto. clear x Hx; intros x IH Hx p n Hn Hp H. Z.le_elim Hx; subst. - apply Z.le_succ_l in Hx; simpl in Hx. Z.le_elim Hx; subst. + case (prime_dec x); intros Hpr. * exists 1; rewrite Z.pow_1_r; apply prime_power_prime with n; auto. * case not_prime_divide with (2 := Hpr); auto. intros p1 ((Hp1, Hpq1),(q1,->)). assert (Hq1 : 0 < q1) by (apply Z.mul_lt_mono_pos_r with p1; lia). destruct (IH p1) with p n as (r1,Hr1). 3-4: assumption. 1-2: lia. -- transitivity (q1 * p1); trivial. exists q1; auto with zarith. -- destruct (IH q1) with p n as (r2,Hr2). 3-4: assumption. 2: lia. ++ split. ** lia. ** rewrite <- (Z.mul_1_r q1) at 1. apply Z.mul_lt_mono_pos_l; auto with zarith. ++ transitivity (q1 * p1); trivial. exists p1; auto with zarith. ++ exists (r2 + r1); subst. symmetry. apply Z.pow_add_r. ** generalize Hq1; case r2; now auto with zarith. ** generalize Hp1; case r1; now auto with zarith. + exists 0; rewrite Z.pow_0_r; auto. - exists n; destruct H as [? H]; rewrite Z.mul_0_r in H; auto. Qed.
imports: ZArith_base ZArithRing Lia Zcomplements Zdiv Znumtheory Zpower