proposition: Theorem Zdivide_Zpower: forall n m, 0 < n -> (forall p i, prime p -> 0 < i -> (p^i | n) -> (p^i | m)) -> (n | m).
proof: Proof. intros n m Hn; generalize m Hn; pattern n; apply prime_induction; auto with zarith; clear n m Hn. intros m H1; contradict H1; auto with zarith. intros p q H Rec m H1 H2. assert (H3: (p | m)). rewrite <- (Zpower_1_r p); apply H2; auto with zarith; rewrite Zpower_1_r; apply Zdivide_factor_r. case (Zmult_interval p q); auto. apply Z.lt_le_trans with 2; auto with zarith; apply prime_ge_2; auto. case H3; intros k Hk; subst. intros Hq Hq1. rewrite (Zmult_comm k); apply Zmult_divide_compat_l. apply Rec; auto. intros p1 i Hp1 Hp2 Hp3. case (Z.eq_dec p p1); intros Hpp1; subst. case (H2 p1 (Z.succ i)); auto with zarith. rewrite Zpower_Zsucc; try apply Zmult_divide_compat_l; auto with zarith. intros q2 Hq2; exists q2. apply Zmult_reg_r with p1. contradict H; subst; apply not_prime_0. rewrite Hq2; rewrite Zpower_Zsucc; try ring; auto with zarith. apply Gauss with p. rewrite Zmult_comm; apply H2; auto. apply Z.divide_trans with (1:= Hp3). apply Zdivide_factor_l. apply rel_prime_sym; apply rel_prime_Zpower_r; auto with zarith. apply prime_rel_prime; auto. contradict Hpp1; apply prime_divide_prime_eq; auto. Qed.
imports: ArithRing ZArith Zpow_facts Znumtheory Tactic