proposition: Theorem prime_div_induction: forall (P: Z -> Prop) n, 0 < n -> (P 1) -> (forall p i, prime p -> 0 <= i -> (p^i | n) -> P (p^i)) -> (forall p q, rel_prime p q -> P p -> P q -> P (p * q)) -> forall m, 0 <= m -> (m | n) -> P m.
proof: Proof. intros P n P1 Hn H H1 m Hm. generalize Hm; pattern m; apply Z_lt_induction; auto; clear m Hm. intros m Rec Hm H2. case (prime_dec m); intros Hm1. rewrite <- Zpower_1_r; apply H; auto with zarith. rewrite Zpower_1_r; auto. case Zle_lt_or_eq with (1 := Hm); clear Hm; intros Hm; subst. 2: contradict P1; case H2; intros; subst; auto with zarith. case (Zle_lt_or_eq 1 m); auto with zarith; clear Hm; intros Hm; subst; auto. case Zdivide_div_prime_le_square with m; auto. intros p (Hp1, (Hp2, Hp3)). case (div_power_max p m); auto with zarith. generalize (prime_ge_2 p Hp1); auto with zarith. intros i (Hi, (Hi1, Hi2)). case Zle_lt_or_eq with (1 := Hi); clear Hi; intros Hi. assert (Hpi: 0 < p ^ i). apply Zpower_gt_0; auto with zarith. apply Z.lt_le_trans with 2; try apply prime_ge_2; auto with zarith. rewrite (Z_div_exact_2 m (p ^ i)); auto with zarith. apply H1; auto with zarith. apply rel_prime_sym; apply rel_prime_Zpower_r; auto with zarith. apply rel_prime_sym. apply prime_rel_prime; auto. contradict Hi2. case Hi1; intros; subst. rewrite Z_div_mult in Hi2; auto with zarith. case Hi2; intros q0 Hq0; subst. exists q0; rewrite Zpower_exp; try rewrite Zpower_1_r; auto with zarith. apply H; auto with zarith. apply Z.divide_trans with (1 := Hi1); auto. apply Rec; auto with zarith. split; auto with zarith. apply Z_div_pos; auto with zarith. apply Z_div_lt; auto with zarith. apply Z.le_ge; apply Z.le_trans with p. apply prime_ge_2; auto. pattern p at 1; rewrite <- Zpower_1_r; apply Zpower_le_monotone; auto with zarith. apply Z.lt_le_trans with 2; try apply prime_ge_2; auto with zarith. apply Z_div_pos; auto with zarith. apply Z.divide_trans with (2 := H2); auto. exists (p ^ i); apply Z_div_exact_2; auto with zarith. apply Zdivide_mod; auto with zarith. apply Zdivide_mod; auto with zarith. case Hi2; rewrite <- Hi; rewrite Zplus_0_r; rewrite Zpower_1_r; auto. Qed.
imports: ArithRing ZArith Zpow_facts Znumtheory Tactic