proposition: Theorem prime_divide_Zpower_Zdiv: forall m a p i, 0 <= i -> prime p -> (m | a) -> ~(m | (a/p)) -> (p^i | a) -> (p^i | m).
proof: Proof. intros m a p i Hi Hp (k, Hk) H (l, Hl); subst. case (Zle_lt_or_eq 0 i); auto with arith; intros Hi1; subst. assert (Hp0: 0 < p). apply Z.lt_le_trans with 2; auto with zarith; apply prime_ge_2; auto. case (Zdivide_dec p k); intros H1. case H1; intros k' H2; subst. case H; replace (k' * p * m) with ((k' * m) * p); try ring; rewrite Z_div_mult; auto with zarith. apply Gauss with k. exists l; rewrite Hl; ring. apply rel_prime_sym; apply rel_prime_Zpower_r; auto. apply rel_prime_sym; apply prime_rel_prime; auto. rewrite Zpower_0_r; apply Zone_divide. Qed.
imports: ArithRing ZArith Zpow_facts Znumtheory Tactic