proposition: Theorem div_power_max: forall p q, 1 < p -> 0 < q -> exists n, 0 <= n /\ (p ^n | q) /\ ~(p ^(1 + n) | q).
proof: Proof. intros p q H1 H2; generalize H2; pattern q; apply Z_lt_induction; auto with zarith; clear q H2. intros q Rec H2. case (Zdivide_dec p q); intros H3. case (Zdivide_Zdiv_lt_pos p q); auto with zarith; intros H4 H5. case (Rec (Z.div q p)); auto with zarith. intros n (Ha1, (Ha2, Ha3)); exists (n + 1); split; auto with zarith; split. case Ha2; intros q1 Hq; exists q1. rewrite Zpower_exp by auto with zarith. rewrite Zpower_1_r by auto with zarith. rewrite Zmult_assoc; rewrite <- Hq. rewrite Zmult_comm; apply Zdivide_Zdiv_eq; auto with zarith. intros (q1, Hu); case Ha3; exists q1. apply Zmult_reg_r with p; auto with zarith. rewrite (Zmult_comm (q / p)); rewrite <- Zdivide_Zdiv_eq by auto with zarith. apply trans_equal with (1 := Hu). rewrite !Zpower_exp by auto with zarith. ring. exists 0; repeat split; try rewrite Zpower_1_r; auto with zarith. Qed.
imports: ArithRing ZArith Zpow_facts Znumtheory Tactic